Searched refs:dst (Results 26 - 50 of 81) sorted by relevance

1234

/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DfunCall.sml96 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 DCFG.sml84 [{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 DIRSyntax.sml33 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 DregAllocation.sml180 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 DfunCall.sml96 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 DCFG.sml84 [{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 DIRSyntax.sml33 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 DregAllocation.sml180 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 Dx64_stepLib.sml898 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 DArraySignature.sml33 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 DArraySliceSignature.sml33 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 DMONO_ARRAY.sml36 val copy : {src : array, dst : array, di : int} -> unit
37 val copyVec : {src : vector, dst : array, di : int} -> unit
H A DMONO_ARRAY_SLICE.sml39 val copy : {src : slice, dst : array, di : int} -> unit
40 val copyVec : {src : vector_slice, dst : array, di : int} -> unit
H A DArray.sml133 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 DWord8Array.sml36 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 DArray2.sml129 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 DCFG.sml83 [{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 DIRSyntax.sml33 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 DregAllocation.sml180 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 DProof.h79 void compress (Proof& dst, ClauseId goal = ClauseId_NULL); // 'dst' should be a newly constructed, empty proof.
H A DProof.C255 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 Dnative_ieeeLib.sml171 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 Dx64Script.sml2671 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 DswsepScript.sml120 (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 Dbasis2002.sml279 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...]

Completed in 185 milliseconds

1234