Name | Date | Size | ||
---|---|---|---|---|
.. | 25-Jul-2019 | 25 | ||
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_opsemScript.sml | H A D | 25-Jul-2019 | 160.5 KiB | |
arm_seq_monadScript.sml | H A D | 25-Jul-2019 | 29.3 KiB | |
arm_stepScript.sml | H A D | 25-Jul-2019 | 177.3 KiB | |
armScript.sml | H A D | 25-Jul-2019 | 4.7 KiB | |
armSyntax.sig | H A D | 25-Jul-2019 | 8.1 KiB | |
armSyntax.sml | H A D | 25-Jul-2019 | 15.3 KiB | |
README | H A D | 25-Jul-2019 | 1.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