-
Notifications
You must be signed in to change notification settings - Fork 1
guancio/armv8bil
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
Formal model of the BIL language and certifying ARMv8 transcompiler * Dependencies HOL4 (tested using the git commit: 6a5443a16aa2f5b5c9d4485224aca15d4a40d6be) * Compilation - create a symbolic link from l3-machine-code to the proper HOL4 directory ln -s <hol_folder>/examples/l3-machine-code l3-machine-code - compile the BIL model and the transcompiler and the HOL4 heap (to speed up loading times) cd bin <hol_folder>/bin/Holmake * Translation of a single instruction in the ./bin directory prepare a file (e.g. test.sml) with the following content HOL_Interactive.toggle_quietdec(); open HolKernel boolLib bossLib Parse; open lcsymtacs utilsLib; open wordsLib blastLib; open state_transformerTheory updateTheory arm8Theory; open stateTheory; open lcsymtacs arm8_stepTheory; open state_transformerSyntax; open arm8_stepLib; open proofTools arithTheory; open bilTheory arm8bilTheory; open arm8bilLib; open arm8stepbilLib; open arm8bilInstructionLib; HOL_Interactive.toggle_quietdec(); val th = tc_one_instruction2_by_bin "d37ff800" ``4w:word64`` ``\x.x<+0x100000w:word64``; print_thm th; Here, "d37ff800" is the hexadecimal representation of the instruction, ``4`` is the address where the instruction is stored and ``\x.x<+0x100000w:word64`` is a property stating where the executable code is stored. From the ./bin directory execute
About
No description, website, or topics provided.
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published