NameDateSize

..25-Jul-201925

arm_astScript.smlH A D25-Jul-20197.9 KiB

arm_astSyntax.sigH A D25-Jul-201927.2 KiB

arm_astSyntax.smlH A D25-Jul-201946.5 KiB

arm_coretypesScript.smlH A D25-Jul-201916.5 KiB

arm_decoderScript.smlH A D25-Jul-201967.9 KiB

arm_opsemScript.smlH A D25-Jul-2019160.5 KiB

arm_seq_monadScript.smlH A D25-Jul-201929.3 KiB

arm_stepScript.smlH A D25-Jul-2019177.3 KiB

armScript.smlH A D25-Jul-20194.7 KiB

armSyntax.sigH A D25-Jul-20198.1 KiB

armSyntax.smlH A D25-Jul-201915.3 KiB

READMEH A D25-Jul-20191.2 KiB

README

1ARM Machine Code Semantics:
2
3 - arm_coretypesScript.sml : specifies underlying types and operations
4 - arm_astScript.sml       : abstract syntax tree (AST) for instructions
5 - arm_decoderScript.sml   : decoding machine code to the AST
6 - arm_seq_monadScript.sml : state-transformer monad - specifies access to
7                             registers and main memory
8 - arm_opsemScript.sml     : operational semantics for instructions
9 - armScript.sml           : running programs (top-level next state function)
10 - arm_stepScript.sml      : definitions and lemmas for "step" theorems
11 - eval/arm_emitScript.sml : use EmitML to produce SML version
12 - eval/arm_evalScript.sml : version with Patricia tree memory
13                             (suited to evaluation)
14
15 - arm_parserLib           : parse ARM assembly code (output to AST)
16 - arm_encoderLib          : encode AST as machine code
17 - arm_disassemblerLib     : convert AST to ARM assembly code
18 - arm_stepLib             : generate "step" theorems
19 - armLib                  : top-level tools
20
21Should work with Poly/ML and Moscow ML.  However, you may need to patch
22Moscow ML, see <http://hol.sourceforge.net/mosml-chr-instructions.html>.
23