Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
..
Failed to load latest commit information.
eval Empty command-line Holmake only builds first target in Holmakefile.
EXAMPLES Minor change capturing unpredictable case for LDM -- from latest ARM …
Holmakefile Another Holmakefile needing fixing after 6e6ca26
README A few changes:
armLib.sig split an include to get Holmake to work
armLib.sml Fix for Thumb-2 decoding of "MSR spsr, <Rn>".
armScript.sml Adopt ML-style syntax for case expressions and use freed up "||" for …
armSyntax.sig Move bit_count constants from examples/ARM/v7 to wordsTheory.
armSyntax.sml Move bit_count constants from examples/ARM/v7 to wordsTheory.
arm_astScript.sml Adopt ML-style syntax for case expressions and use freed up "||" for …
arm_astSyntax.sig Update that adds support for ThumbEE.
arm_astSyntax.sml Update that adds support for ThumbEE.
arm_coretypesScript.sml Move bit_count constants from examples/ARM/v7 to wordsTheory.
arm_decoderScript.sml change interface to add_persistent_funs (#73) and fix more calls
arm_disassemblerLib.sig A few refinements. Also added an examples file, which demonstrates how
arm_disassemblerLib.sml Fix in the printing of BFC and BFI instructions.
arm_encoderLib.sig Minor change capturing unpredictable case for LDM -- from latest ARM …
arm_encoderLib.sml Minor change capturing unpredictable case for LDM -- from latest ARM …
arm_opsemScript.sml change interface to add_persistent_funs (#73) and fix more calls
arm_parserLib.sig Minor change capturing unpredictable case for LDM -- from latest ARM …
arm_parserLib.sml Move bit_count constants from examples/ARM/v7 to wordsTheory.
arm_random_testingLib.sig Update that adds support for ThumbEE.
arm_random_testingLib.sml Minor change to the predictability of the CPS instruction, to keep up…
arm_seq_monadScript.sml Minor tweaks to comments.
arm_stepLib.sig A new Monadic ARM instruction set specification. Covers all current ISA
arm_stepLib.sml Improvements to updateLib. Added some comments describing the various…
arm_stepScript.sml Remove the constant bit$LSB, which was simply arithmetic$ODD. This ma…
example.s A few refinements. Also added an examples file, which demonstrates how
selftest.sml Support for evaluating instructions of the form "ldr pc,[pc,rn,lsl #2]".

README

ARM Machine Code Semantics:

 - arm_coretypesScript.sml : specifies underlying types and operations
 - arm_astScript.sml       : abstract syntax tree (AST) for instructions
 - arm_decoderScript.sml   : decoding machine code to the AST
 - arm_seq_monadScript.sml : state-transformer monad - specifies access to
                             registers and main memory
 - arm_opsemScript.sml     : operational semantics for instructions
 - armScript.sml           : running programs (top-level next state function)
 - arm_stepScript.sml      : definitions and lemmas for "step" theorems
 - eval/arm_emitScript.sml : use EmitML to produce SML version
 - eval/arm_evalScript.sml : version with Patricia tree memory
                             (suited to evaluation)

 - arm_parserLib           : parse ARM assembly code (output to AST)
 - arm_encoderLib          : encode AST as machine code
 - arm_disassemblerLib     : convert AST to ARM assembly code
 - arm_stepLib             : generate "step" theorems
 - armLib                  : top-level tools

Should work with Poly/ML and Moscow ML.  However, you may need to patch
Moscow ML, see <http://hol.sourceforge.net/mosml-chr-instructions.html>.
Something went wrong with that request. Please try again.