/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | assemblerML.sig | 8 val num_to_arm : Arbnum.num -> Data.instruction 9 val arm_to_num : Data.instruction -> Arbnum.num 10 val arm_to_string : Arbnum.num option -> bool -> Data.instruction -> string 11 val string_to_arm : string -> Data.instruction 13 Arbnum.num -> Data.instruction 24 val validate_instruction : Data.instruction -> Data.instruction
|
H A D | instructionSyntax.sml | 47 AND => ``instruction$AND`` | EOR => ``instruction$EOR`` 48 | SUB => ``instruction$SUB`` | RSB => ``instruction$RSB`` 49 | ADD => ``instruction$ADD`` | ADC => ``instruction$ADC`` 50 | SBC => ``instruction$SBC`` | RSC => ``instruction$RSC`` 51 | TST => ``instruction$TST`` | TEQ => ``instruction [all...] |
H A D | instructionSyntax.sig | 5 val arm_to_term : Data.instruction -> term 6 val term_to_arm : term -> Data.instruction
|
H A D | arm_evalScript.sml | 3 (* DESCRIPTION : Various theorems about the ISA and instruction encoding *) 536 `(!cond offset. DECODE_ARM (enc (instruction$B cond offset)) = br) /\ 537 (!cond offset. DECODE_ARM (enc (instruction$BL cond offset)) = br)`, 541 `!cond. DECODE_ARM (enc (instruction$SWI cond)) = swi_ex`, 557 `!f. f IN {instruction$AND; instruction$EOR; 558 instruction$SUB; instruction$RSB; 559 instruction$ADD; instruction [all...] |
H A D | arm_rulesScript.sml | 242 val ARM_AND_NOP = eval_nop ``instruction$AND`` 243 val ARM_EOR_NOP = eval_nop ``instruction$EOR`` 244 val ARM_SUB_NOP = eval_nop ``instruction$SUB`` 245 val ARM_RSB_NOP = eval_nop ``instruction$RSB`` 246 val ARM_ADD_NOP = eval_nop ``instruction$ADD`` 247 val ARM_ADC_NOP = eval_nop ``instruction$ADC`` 248 val ARM_SBC_NOP = eval_nop ``instruction$SBC`` 249 val ARM_RSC_NOP = eval_nop ``instruction$RSC`` 250 val ARM_ORR_NOP = eval_nop ``instruction$ORR`` 251 val ARM_BIC_NOP = eval_nop ``instruction [all...] |
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/decompiler/ |
H A D | arm_core_decompLib.sig | 4 val l3_triple: string -> helperLib.instruction 5 val l3_triple_code: string quotation -> helperLib.instruction list
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/decompiler/ |
H A D | m0_core_decompLib.sig | 4 val m0_triple: string -> helperLib.instruction 5 val m0_triple_code: string quotation -> helperLib.instruction list
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | file_readerLib.sig | 9 val arm_spec : string -> helperLib.instruction 10 val m0_spec : string -> helperLib.instruction 11 val riscv_spec : string -> helperLib.instruction
|
H A D | derive_specsLib.sml | 497 val ((pos,instruction,asm)::code) = code 498 val ((pos,instruction,asm)::code) = drop 1 code 499 val ((pos,instruction,asm)::code) = drop 17 code 502 | get_specs ((pos,instruction,asm)::code) = let 503 val instruction = delete_spaces instruction value 505 if String.isPrefix "call:" instruction then let 506 val ts = String.tokens (fn x => x = #":") instruction 508 val instruction = ts |> el 3 value 516 val res = wrap_get_spec f instruction [all...] |
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
H A D | core_decompilerLib.sig | 9 triple_fn: string -> helperLib.instruction,
|
/seL4-l4v-master/graph-refine/graph-to-graph/chronos/ |
H A D | parser.py | 10 Regular expression based single instruction parsing utility. 18 The following constants culminate to valid_instruction_re, a regex search pattern, which is used to decipher an instruction mnemonic into the base instruction and all the 84 # The following regexes take the arguments of a specific instruction (whose 86 # from the instruction. 189 '''ARM ldr/str[bh] instruction.''' 262 '''ARM ldm*/stm* instruction.''' 321 # Translate us into a ldm/stm instruction. 337 '''ARM arithmetic instruction with 3 arguments and the result is stored 385 '''ARM move instruction wit [all...] |
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_parserLib.sig | 41 {label:} {instruction | directive} 47 - an instruction is in ARM UAL (Unified Assembler Language) syntax 86 b.n +#4 ; branch to the next instruction 87 b -#8 /* branches to the labelled instruction
|
/seL4-l4v-master/seL4/src/arch/arm/armv/armv8-a/64/ |
H A D | cache.c | 37 static inline word_t readCacheSize(int level, bool_t instruction) argument 43 MSR("csselr_el1", ((level << 1) | instruction));
|
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
H A D | arm_evalScript.sml | 45 | NONE => errorT "couldn't fetch an instruction") 46 | NONE => errorT "couldn't fetch an instruction") 47 | NONE => errorT "couldn't fetch an instruction") 48 | NONE => errorT "couldn't fetch an instruction")`; 57 | NONE => errorT "couldn't fetch an instruction") 58 | NONE => errorT "couldn't fetch an instruction"`;
|
/seL4-l4v-master/seL4/src/arch/arm/armv/armv7-a/ |
H A D | cache.c | 41 static inline word_t readCacheSize(int level, bool_t instruction) argument 47 asm volatile("mcr p15, 2, %0, c0, c0, 0" : : "r"((level << 1) | instruction));
|
/seL4-l4v-master/seL4/src/arch/arm/armv/armv8-a/32/ |
H A D | cache.c | 41 static inline word_t readCacheSize(int level, bool_t instruction) argument 47 asm volatile("mcr p15, 2, %0, c0, c0, 0" : : "r"((level << 1) | instruction));
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_Script.sml | 32 let n = 20 - (LENGTH w DIV 8) in (* calc length of instruction *) 34 then x86_execute_some i (n2w n) s else NONE (* execute the instruction *)`;
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_Script.sml | 32 let n = 20 - (LENGTH w DIV 8) in (* calc length of instruction *) 34 then x64_execute_some i (n2w n) s else NONE (* execute the instruction *)`;
|
/seL4-l4v-master/HOL4/examples/computability/register/ |
H A D | register_machineScript.sml | 14 val _ = Datatype `instruction = Inc num | Dec num | JZ num num bool`; 16 val _ = Datatype `RegMachine = <| insts : instruction list; regs : num |-> num; pc : num |>`; 142 Jump (z) = jump to instruction z = JZ(r0,z) for an r0 that contains 0 151 Composition ~ Concatination of instruction? 159 Then we need to show Turing Machine can simulate the original 3 instruction set
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/model/ |
H A D | riscvScript.sml | 328 [("instruction", 340 [("F_Error",[CTy"instruction"]),("F_Result",[CTy"rawInstType"])])] 10756 ("Run",Var("v0",CTy"instruction"), 10759 CS(Var("v0",CTy"instruction"), 10760 [(Const("UnknownInstruction",CTy"instruction"), 10763 ("FENCE",CTy"instruction", 10766 ("FENCE_I",CTy"instruction", 10768 (Call("AMO",CTy"instruction",Var("v1",CTy"AMO")), 10958 (Call("ArithI",CTy"instruction",Var("v24",CTy"ArithI")), 11019 (Call("ArithR",CTy"instruction",Va [all...] |
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/ |
H A D | armScript.sml | 314 [("instruction", 14725 ("Run",Var("v0",CTy"instruction"), 14728 CS(Var("v0",CTy"instruction"), 14729 [(Const("ClearExclusive",CTy"instruction"), 14731 (Const("NoOperation",CTy"instruction"), 14734 ("Divide",CTy"instruction", 14740 (Call("IfThen",CTy"instruction",Var("v153",PTy(F4,F4))), 14745 ("Swap",CTy"instruction", 14751 (Call("Undefined",CTy"instruction",Var("v155",F32)), 14755 (Call("Branch",CTy"instruction",Va [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sig | 6 type instruction = type 11 (string -> instruction) * (term -> term -> int -> bool -> string * int) * 34 val instruction_apply : (thm -> thm) -> instruction -> instruction
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64Script.sml | 128 [("instruction", 156 ("Zfull_inst",[PTy(LTy F8,PTy(CTy"instruction",OTy(LTy F8)))])])] 5289 ("Run",Var("v0",CTy"instruction"), 5292 CS(Var("v0",CTy"instruction"), 5293 [(Const("Zclc",CTy"instruction"), 5295 (Const("Zcmc",CTy"instruction"), 5297 (Const("Zleave",CTy"instruction"), 5299 (Const("Zstc",CTy"instruction"), 5302 ("Zbinop",CTy"instruction", 5312 ("Zbit_test",CTy"instruction", [all...] |
/seL4-l4v-master/HOL4/examples/l3-machine-code/mips/model/ |
H A D | mipsScript.sml | 283 [("instruction", 7477 LS"Unpredictable instruction")),qVar"state"))) 7480 ("Run",Var("v0",CTy"instruction"), 7483 CS(Var("v0",CTy"instruction"), 7484 [(Const("BREAK",CTy"instruction"), 7486 (Const("ERET",CTy"instruction"), 7488 (Const("ReservedInstruction",CTy"instruction"), 7491 (Const("SYSCALL",CTy"instruction"), 7493 (Const("TLBP",CTy"instruction"), 7495 (Const("TLBR",CTy"instruction"), [all...] |
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/model/ |
H A D | arm8Script.sml | 352 [("instruction", 2486 ("Run",Var("v0",CTy"instruction"), 2489 CS(Var("v0",CTy"instruction"), 2490 [(Const("Reserved",CTy"instruction"), 2492 (Const("Unallocated",CTy"instruction"), 2495 ("Address",CTy"instruction", 2501 (Call("ClearExclusive",CTy"instruction",Var("v82",F4)), 2505 (Call("Hint",CTy"instruction",Var("v83",CTy"SystemHintOp")), 2510 ("MemoryBarrier",CTy"instruction", 2516 (Call("Branch",CTy"instruction",Va [all...] |