Name | Date | Size | ||
---|---|---|---|---|
.. | 25-Jul-2019 | 6 | ||
arm_astScript.sml | H A D | 25-Jul-2019 | 7.9 KiB | |
arm_astSyntax.sig | H A D | 25-Jul-2019 | 27.2 KiB | |
arm_astSyntax.sml | H A D | 25-Jul-2019 | 46.5 KiB | |
arm_coretypesScript.sml | H A D | 25-Jul-2019 | 16.5 KiB | |
arm_decoderScript.sml | H A D | 25-Jul-2019 | 67.9 KiB | |
arm_disassemblerLib.sig | H A D | 25-Jul-2019 | 108 | |
arm_disassemblerLib.sml | H A D | 25-Jul-2019 | 32 KiB | |
arm_encoderLib.sig | H A D | 25-Jul-2019 | 653 | |
arm_encoderLib.sml | H A D | 25-Jul-2019 | 64.3 KiB | |
arm_opsemScript.sml | H A D | 25-Jul-2019 | 159.6 KiB | |
arm_parserLib.sig | H A D | 25-Jul-2019 | 2.9 KiB | |
arm_parserLib.sml | H A D | 25-Jul-2019 | 197.7 KiB | |
arm_random_testingLib.sig | H A D | 25-Jul-2019 | 1.1 KiB | |
arm_random_testingLib.sml | H A D | 25-Jul-2019 | 45.3 KiB | |
arm_seq_monadScript.sml | H A D | 25-Jul-2019 | 29 KiB | |
arm_stepLib.sig | H A D | 25-Jul-2019 | 182 | |
arm_stepLib.sml | H A D | 25-Jul-2019 | 51 KiB | |
arm_stepScript.sml | H A D | 25-Jul-2019 | 177.3 KiB | |
armLib.sig | H A D | 25-Jul-2019 | 3.6 KiB | |
armLib.sml | H A D | 25-Jul-2019 | 9.3 KiB | |
armScript.sml | H A D | 25-Jul-2019 | 4.7 KiB | |
armSyntax.sig | H A D | 25-Jul-2019 | 8 KiB | |
armSyntax.sml | H A D | 25-Jul-2019 | 14.9 KiB | |
eval/ | H | 25-Jul-2019 | 10 | |
example.s | H A D | 25-Jul-2019 | 97 | |
EXAMPLES | H A D | 25-Jul-2019 | 21.9 KiB | |
Holmakefile | H A D | 25-Jul-2019 | 236 | |
README | H A D | 25-Jul-2019 | 1.2 KiB | |
selftest.sml | H A D | 25-Jul-2019 | 21.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