NameDateSize

..25-Jul-20196

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_disassemblerLib.sigH A D25-Jul-2019108

arm_disassemblerLib.smlH A D25-Jul-201932 KiB

arm_encoderLib.sigH A D25-Jul-2019653

arm_encoderLib.smlH A D25-Jul-201964.3 KiB

arm_opsemScript.smlH A D25-Jul-2019159.6 KiB

arm_parserLib.sigH A D25-Jul-20192.9 KiB

arm_parserLib.smlH A D25-Jul-2019197.7 KiB

arm_random_testingLib.sigH A D25-Jul-20191.1 KiB

arm_random_testingLib.smlH A D25-Jul-201945.3 KiB

arm_seq_monadScript.smlH A D25-Jul-201929 KiB

arm_stepLib.sigH A D25-Jul-2019182

arm_stepLib.smlH A D25-Jul-201951 KiB

arm_stepScript.smlH A D25-Jul-2019177.3 KiB

armLib.sigH A D25-Jul-20193.6 KiB

armLib.smlH A D25-Jul-20199.3 KiB

armScript.smlH A D25-Jul-20194.7 KiB

armSyntax.sigH A D25-Jul-20198 KiB

armSyntax.smlH A D25-Jul-201914.9 KiB

eval/H25-Jul-201910

example.sH A D25-Jul-201997

EXAMPLESH A D25-Jul-201921.9 KiB

HolmakefileH A D25-Jul-2019236

READMEH A D25-Jul-20191.2 KiB

selftest.smlH A D25-Jul-201921.4 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