Searched refs:instruction (Results 1 - 25 of 121) sorted by relevance

12345

/seL4-l4v-master/HOL4/examples/ARM/v4/
H A DassemblerML.sig8 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 DinstructionSyntax.sml47 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 DinstructionSyntax.sig5 val arm_to_term : Data.instruction -> term
6 val term_to_arm : term -> Data.instruction
H A Darm_evalScript.sml3 (* 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 Darm_rulesScript.sml242 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 Darm_core_decompLib.sig4 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 Dm0_core_decompLib.sig4 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 Dfile_readerLib.sig9 val arm_spec : string -> helperLib.instruction
10 val m0_spec : string -> helperLib.instruction
11 val riscv_spec : string -> helperLib.instruction
H A Dderive_specsLib.sml497 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 Dcore_decompilerLib.sig9 triple_fn: string -> helperLib.instruction,
/seL4-l4v-master/graph-refine/graph-to-graph/chronos/
H A Dparser.py10 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 Darm_parserLib.sig41 {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 Dcache.c37 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 Darm_evalScript.sml45 | 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 Dcache.c41 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 Dcache.c41 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 Dx86_Script.sml32 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 Dx64_Script.sml32 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 Dregister_machineScript.sml14 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 DriscvScript.sml328 [("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 DarmScript.sml314 [("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 DhelperLib.sig6 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 Dx64Script.sml128 [("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 DmipsScript.sml283 [("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 Darm8Script.sml352 [("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...]

Completed in 343 milliseconds

12345