/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | funCall.sml | 96 fun one_stm ({oper = op1, dst = dst1, src = src1}) = 97 {oper = op1, dst = List.map filter_mems dst1, src = List.map filter_mems src1} 131 fun dec_p pt n = {oper = IR.msub, dst = [IR.REG pt], src = [IR.REG pt, IR.WCONST (Arbint.fromInt (4*n))]} 133 fun inc_p pt n = {oper = IR.madd, dst = [IR.REG pt], src = [IR.REG pt, IR.WCONST (Arbint.fromInt (4*n))]}; 147 [ {oper = IR.mmov, dst = [IR.REG (IR.fromAlias IR.ip)], src = [IR.REG (IR.fromAlias IR.sp)]}, 148 {oper = IR.mpush, dst = [IR.REG (IR.fromAlias IR.sp)], 152 {oper = IR.msub, dst = [IR.REG (IR.fromAlias IR.fp)], src = [IR.REG (IR.fromAlias IR.ip), IR.WCONST (Arbint.fromInt 4)]}, 163 {oper = IR.msub, dst = [IR.REG (IR.fromAlias IR.sp)], src = [IR.REG (IR.fromAlias IR.fp), IR.WCONST (Arbint.fromInt (4* (3 + length rs)))]}, 164 {oper = IR.mpop, dst = rs @ [IR.REG (IR.fromAlias IR.fp), IR.REG (IR.fromAlias IR.sp), IR.REG (IR.fromAlias IR.pc)], 210 {oper = IR.mldr, dst [all...] |
H A D | CFG.sml | 84 [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 88 ({ instr = Assem.OPER {oper = (bi_operator bop,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 96 [{ instr = Assem.OPER {oper = (Assem.CMP,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 105 dst = [one_exp d], 113 [{ instr = Assem.MOVE {dst = one_exp d, src = one_exp s}, 118 [{ instr = Assem.OPER {oper = (Assem.B,SOME Assem.AL,false), dst = [], src = [], jump = SOME [lab]}, 123 [{ instr = Assem.OPER {oper = (Assem.B, SOME (cjump (getTmp e)), false), dst = [], src = [one_exp e], jump = SOME [lab]}, 174 val augmentedInsts = ({instr = Assem.OPER{oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 176 insts @ [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE},
|
H A D | IRSyntax.sml | 33 type instr = {oper: operator, dst: exp list, src: exp list} 234 fun convert_stm ({oper = op1, dst = dlist, src = slist}) = 319 fun to_inst (Assem.OPER {oper = (oper', cond', flag'), dst = dlist, src = slist, jump = jumps}) = 320 {oper = to_op oper', dst = List.map to_exp dlist, src = List.map to_exp slist} 321 | to_inst (Assem.MOVE {dst = dst', src = src'}) = 322 {oper = mmov, dst = [to_exp dst'], src = [to_exp src']} 326 fun to_cond (Assem.OPER {oper = (Assem.CMP, cond1, flag1), dst = dlist1, src = slist1, jump = jumps1}, 327 Assem.OPER {oper = (Assem.B, cond2, flag2), dst [all...] |
H A D | regAllocation.sml | 180 fun isMoveInst (Assem.MOVE {dst = Assem.TEMP d1, src = Assem.TEMP s1}) = true 191 ( let val (dst,src) = (#def inst, #use inst) in value 193 T.enter(def, nodeNo, S.addList(S.empty intOrder, dst))) 608 fun substituteVars (Assem.OPER {oper = p, dst = d1, src = s1, jump = j1}) old new rhs lhs = 609 Assem.OPER {oper = p, dst = if rhs then replace d1 old new else d1, 612 | substituteVars (Assem.MOVE {dst = d1, src = s1}) old new rhs lhs = 613 Assem.MOVE {dst = if rhs andalso d1 = old then new else d1, 646 dst = [Assem.TEMP newVarNo], 661 dst = [Assem.TMEM (!memIndex)], 683 let val (Assem.MOVE {dst [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | funCall.sml | 96 fun one_stm ({oper = op1, dst = dst1, src = src1}) = 97 {oper = op1, dst = List.map filter_mems dst1, src = List.map filter_mems src1} 128 fun dec_p pt n = {oper = IR.msub, dst = [IR.REG pt], src = [IR.REG pt, IR.WCONST (Arbint.fromInt n)]} 130 fun inc_p pt n = {oper = IR.madd, dst = [IR.REG pt], src = [IR.REG pt, IR.WCONST (Arbint.fromInt n)]}; 144 [ {oper = IR.mmov, dst = [IR.REG (IR.fromAlias IR.ip)], src = [IR.REG (IR.fromAlias IR.sp)]}, 145 {oper = IR.mpush, dst = [IR.REG (IR.fromAlias IR.sp)], 149 {oper = IR.msub, dst = [IR.REG (IR.fromAlias IR.fp)], src = [IR.REG (IR.fromAlias IR.ip), IR.WCONST Arbint.one]}, 160 {oper = IR.msub, dst = [IR.REG (IR.fromAlias IR.sp)], src = [IR.REG (IR.fromAlias IR.fp), IR.WCONST (Arbint.fromInt (3 + length rs))]}, 161 {oper = IR.mpop, dst = rs @ [IR.REG (IR.fromAlias IR.fp), IR.REG (IR.fromAlias IR.sp), IR.REG (IR.fromAlias IR.pc)], 207 {oper = IR.mldr, dst [all...] |
H A D | CFG.sml | 84 [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 88 ({ instr = Assem.OPER {oper = (bi_operator bop,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 96 [{ instr = Assem.OPER {oper = (Assem.CMP,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 105 dst = [one_exp d], 113 [{ instr = Assem.MOVE {dst = one_exp d, src = one_exp s}, 118 [{ instr = Assem.OPER {oper = (Assem.B,SOME Assem.AL,false), dst = [], src = [], jump = SOME [lab]}, 123 [{ instr = Assem.OPER {oper = (Assem.B, SOME (cjump (getTmp e)), false), dst = [], src = [one_exp e], jump = SOME [lab]}, 174 val augmentedInsts = ({instr = Assem.OPER{oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 176 insts @ [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE},
|
H A D | IRSyntax.sml | 33 type instr = {oper: operator, dst: exp list, src: exp list} 234 fun convert_stm ({oper = op1, dst = dlist, src = slist}) = 319 fun to_inst (Assem.OPER {oper = (oper', cond', flag'), dst = dlist, src = slist, jump = jumps}) = 320 {oper = to_op oper', dst = List.map to_exp dlist, src = List.map to_exp slist} 321 | to_inst (Assem.MOVE {dst = dst', src = src'}) = 322 {oper = mmov, dst = [to_exp dst'], src = [to_exp src']} 326 fun to_cond (Assem.OPER {oper = (Assem.CMP, cond1, flag1), dst = dlist1, src = slist1, jump = jumps1}, 327 Assem.OPER {oper = (Assem.B, cond2, flag2), dst [all...] |
H A D | regAllocation.sml | 180 fun isMoveInst (Assem.MOVE {dst = Assem.TEMP d1, src = Assem.TEMP s1}) = true 191 ( let val (dst,src) = (#def inst, #use inst) in value 193 T.enter(def, nodeNo, S.addList(S.empty intOrder, dst))) 608 fun substituteVars (Assem.OPER {oper = p, dst = d1, src = s1, jump = j1}) old new rhs lhs = 609 Assem.OPER {oper = p, dst = if rhs then replace d1 old new else d1, 612 | substituteVars (Assem.MOVE {dst = d1, src = s1}) old new rhs lhs = 613 Assem.MOVE {dst = if rhs andalso d1 = old then new else d1, 646 dst = [Assem.TEMP newVarNo], 661 dst = [Assem.TMEM (!memIndex)], 683 let val (Assem.MOVE {dst [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/step/ |
H A D | x64_stepLib.sml | 898 val bin_PD = sse_bin ``dfn'bin_PD (f, dst, xmm)`` 899 val bin_SD = sse_bin ``dfn'bin_SD (f, dst, xmm)`` 900 val bin_PS = sse_bin ``dfn'bin_PS (f, dst, xmm)`` 901 val bin_SS = sse_bin ``dfn'bin_SS (f, dst, xmm)`` 903 val logic_PD = sse_logic ``dfn'logic_PD (f, dst, xmm)`` 904 val logic_PS = sse_logic ``dfn'logic_PS (f, dst, xmm)`` 906 val CMPPD = sse_compare ``dfn'CMPPD (f, dst, xmm)`` 907 val CMPSD = sse_compare ``dfn'CMPSD (f, dst, xmm)`` 908 val CMPPS = sse_compare ``dfn'CMPPS (f, dst, xmm)`` 909 val CMPSS = sse_compare ``dfn'CMPSS (f, dst, xm [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | ArraySignature.sml | 33 val copy : {src : 'a array, dst : 'a array, di : int} -> unit 34 val copyVec : {src : 'a vector, dst : 'a array, di : int} -> unit
|
H A D | ArraySliceSignature.sml | 33 val copy : {src : 'a slice, dst : 'a array, di : int} -> unit 34 val copyVec : {src : 'a VectorSlice.slice, dst : 'a array, di : int} -> unit
|
H A D | MONO_ARRAY.sml | 36 val copy : {src : array, dst : array, di : int} -> unit 37 val copyVec : {src : vector, dst : array, di : int} -> unit
|
H A D | MONO_ARRAY_SLICE.sml | 39 val copy : {src : slice, dst : array, di : int} -> unit 40 val copyVec : {src : vector_slice, dst : array, di : int} -> unit
|
H A D | Array.sml | 133 fun copy {src: 'a array as s, dst: 'a array as d, di: int} = 137 if di < 0 orelse di+len > length dst 143 fun copyVec {src: 'a vector, dst: 'a array as d, di: int} = 147 if di < 0 orelse di+len > length dst 253 fun copy {src = Slice{array=s, start=srcStart, length=srcLen}, dst, di: int} = 257 else (Array.update(dst, n+di, Array.sub(s, n+srcStart)); copyUp(n+1)) 261 else (Array.update(dst, n+di, Array.sub(s, n+srcStart)); copyDown(n-1)) 263 if di < 0 orelse di+srcLen > Array.length dst 271 fun copyVec {src: 'a VectorSlice.slice, dst: 'a array as d, di: int} = 275 if di < 0 orelse di+len > Array.length dst [all...] |
H A D | Word8Array.sml | 36 fun System_move_str(src: vector, dst: address, srcOffset: word, dstOffset: word, length: word): unit = 37 RunCall.moveBytes(src, RunCall.unsafeCast dst, srcOffset, dstOffset, length) 209 fun copy {src=Array (len, s), dst=Array (dlen, d), di: int} = 219 fun copyVec {src, dst=Array (dlen, d), di: int} = 371 fun copy {src, dst, di: int} = 375 if di < 0 orelse di+length > Word8Array.length dst 384 else (Word8Array.update(dst, n+di, Word8Array.sub(src, n+start)); copyUp(n+1)) 388 else (Word8Array.update(dst, n+di, Word8Array.sub(src, n+start)); copyDown(n-1)) 395 fun copyVec {src: Word8VectorSlice.slice, dst=Array (dlen, d), di: int} =
|
H A D | Array2.sml | 129 fun copy {src as {base, row, col, ...}, dst, dst_row, dst_col} = 133 val (dRows, dCols) = dimensions dst 140 uncheckedUpdate(dst, dst_row+r, dst_col+c, 150 uncheckedUpdate(dst, dst_row+r, dst_col+c, 159 else (* We have to be careful if dst = src and the regions
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | CFG.sml | 83 [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 87 ({ instr = Assem.OPER {oper = (bi_operator bop,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 95 [{ instr = Assem.OPER {oper = (Assem.CMP,NONE,false), dst = [one_exp d], src = [one_exp e1, one_exp e2], jump = NONE}, 104 dst = [one_exp d], 112 [{ instr = Assem.MOVE {dst = one_exp d, src = one_exp s}, 117 [{ instr = Assem.OPER {oper = (Assem.B,SOME Assem.AL,false), dst = [], src = [], jump = SOME [lab]}, 122 [{ instr = Assem.OPER {oper = (Assem.B, SOME (cjump (getTmp e)), false), dst = [], src = [one_exp e], jump = SOME [lab]}, 173 val augmentedInsts = ({instr = Assem.OPER{oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE}, 175 insts @ [{instr = Assem.OPER {oper = (Assem.NOP,NONE,false), dst = [], src = [], jump = NONE},
|
H A D | IRSyntax.sml | 33 type instr = {oper: operator, dst: exp list, src: exp list} 234 fun convert_stm ({oper = op1, dst = dlist, src = slist}) = 327 fun to_inst (Assem.OPER {oper = (oper', cond', flag'), dst = dlist, src = slist, jump = jumps}) = 328 {oper = to_op oper', dst = List.map to_exp dlist, src = List.map to_exp slist} 329 | to_inst (Assem.MOVE {dst = dst', src = src'}) = 330 {oper = mmov, dst = [to_exp dst'], src = [to_exp src']} 334 fun to_cond (Assem.OPER {oper = (Assem.CMP, cond1, flag1), dst = dlist1, src = slist1, jump = jumps1}, 335 Assem.OPER {oper = (Assem.B, cond2, flag2), dst [all...] |
H A D | regAllocation.sml | 180 fun isMoveInst (Assem.MOVE {dst = Assem.TEMP d1, src = Assem.TEMP s1}) = true 191 ( let val (dst,src) = (#def inst, #use inst) in value 193 T.enter(def, nodeNo, S.addList(S.empty intOrder, dst))) 608 fun substituteVars (Assem.OPER {oper = p, dst = d1, src = s1, jump = j1}) old new rhs lhs = 609 Assem.OPER {oper = p, dst = if rhs then replace d1 old new else d1, 612 | substituteVars (Assem.MOVE {dst = d1, src = s1}) old new rhs lhs = 613 Assem.MOVE {dst = if rhs andalso d1 = old then new else d1, 646 dst = [Assem.TEMP newVarNo], 661 dst = [Assem.TMEM (!memIndex)], 683 let val (Assem.MOVE {dst [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Proof.h | 79 void compress (Proof& dst, ClauseId goal = ClauseId_NULL); // 'dst' should be a newly constructed, empty proof.
|
H A D | Proof.C | 255 void Proof::compress(Proof& dst, ClauseId goal) argument 284 dst.beginChain(chain_id[0]); 286 dst.resolve(chain_var[i-1] & 1 ? -1*chain_id[i] : chain_id[i],chain_var[i-1] >> 1); 287 c2c[id] = dst.endChain(); 309 c2c[id] = dst.addRoot(clause,orig_root_id);
|
/seL4-l4v-10.1.1/HOL4/src/floating-point/native/ |
H A D | native_ieeeLib.sml | 171 fun lift1 f dst tm = 172 case Lib.total dst tm of 179 fun lift2 f dst tm = 180 case Lib.total dst tm of 188 fun liftOrder f dst tm = 189 case Lib.total dst tm of
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64Script.sml | 2671 TP[Var("bop",CTy"sse_binop"),Var("dst",FTy 3),Var("src",CTy"xmm_mem")], 2674 Let(Var("dst",CTy"xmm_mem"), 2675 Call("xmm_reg",CTy"xmm_mem",Var("dst",FTy 3)), 2678 (Call("XMM",ATy(qTy,FTy 128),Var("dst",CTy"xmm_mem")), 2705 Var("dst",CTy"xmm_mem")]), 2714 TP[Var("bop",CTy"sse_binop"),Var("dst",FTy 3),Var("src",CTy"xmm_mem")], 2717 Let(Var("dst",CTy"xmm_mem"), 2718 Call("xmm_reg",CTy"xmm_mem",Var("dst",FTy 3)), 2721 (Call("XMM",ATy(qTy,FTy 128),Var("dst",CTy"xmm_mem")), 2768 Var("dst",CT [all...] |
/seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/ |
H A D | swsepScript.sml | 120 (IS_MEMORY_DOPER (MLDR dst src) = T) /\ 121 (IS_MEMORY_DOPER (MSTR src dst) = T) /\ 122 (IS_MEMORY_DOPER (MPUSH dst' srcL) = T) /\ 123 (IS_MEMORY_DOPER (MPOP dst' srcL) = T) /\ 127 (IS_WELL_FORMED_DOPER (MMUL dst src1 src2) = ~(dst = src1)) /\ 195 (STACK_SIZE_DOPER (MMOV dst e) = (0, 0, ~(dst = R13))) /\ 196 (STACK_SIZE_DOPER (MADD dst reg1 e) = (0, 0, ~(dst [all...] |
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | basis2002.sml | 279 val copy : {src : 'a array, dst : 'a array, di : int} -> unit 280 val copyVec : {src : 'a vector, dst : 'a array, di : int} -> unit 305 fun copy {di,dst,src} = 306 A.copy {src = src, si = 0, len = NONE, dst = dst, di = di} 307 fun copyVec {di,dst,src} = 308 A.copyVec {src = src, si = 0, len = NONE, dst = dst, di = di} 356 dst : 'a Array.array, 361 dst [all...] |