Changeset 3095
 Timestamp:
 Apr 4, 2013, 9:53:30 PM (4 years ago)
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

driver/extracted/policyStep.ml
r3043 r3095 95 95 Types.pi1 96 96 (FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ acc > 97 let prefixlen = List.length prefix in 98 let bvprefixlen = 99 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 100 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 101 (Nat.S (Nat.S Nat.O)))))))))))))))) prefixlen 102 in 103 let bvSprefixlen = 104 Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 105 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 106 (Nat.S Nat.O)))))))))))))))) bvprefixlen 107 in 97 108 (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } = 98 109 Types.pi1 acc … … 105 116  ASM.Instruction i > 106 117 PolicyFront.jump_expansion_step_instruction (Types.pi1 labels) 107 (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix)i118 (Types.pi1 old_sigma) inc_pc_sigma prefixlen i 108 119  ASM.Comment x0 > Types.None 109 120  ASM.Cost x0 > Types.None … … 111 122 Types.Some 112 123 (PolicyFront.select_jump_length (Types.pi1 labels) 113 (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix)j)124 (Types.pi1 old_sigma) inc_pc_sigma prefixlen j) 114 125  ASM.Jnz (x0, x1, x2) > Types.None 115 126  ASM.Call c > 116 127 Types.Some 117 128 (PolicyFront.select_call_length (Types.pi1 labels) 118 (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix)c)129 (Types.pi1 old_sigma) inc_pc_sigma prefixlen c) 119 130  ASM.Mov (x0, x1, x2) > Types.None 120 131 in … … 123 134 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 124 135 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 125 (Nat.S Nat.O)))))))))))))))) 126 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 127 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 128 (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length prefix)) 136 (Nat.S Nat.O)))))))))))))))) bvprefixlen 129 137 (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd = 130 138 Assembly.Short_jump }).Types.snd … … 152 160 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 153 161 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 154 (Nat.S Nat.O)))))))))))))))) 155 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 156 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 157 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S 158 (List.length prefix))) (Types.pi1 old_sigma).Types.snd 159 { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.snd 162 (Nat.S Nat.O)))))))))))))))) bvSprefixlen 163 (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd = 164 Assembly.Short_jump }).Types.snd 160 165 in 161 166 let updated_sigma = 162 167 BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 163 168 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 164 (Nat.S Nat.O)))))))))))))))) 165 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 166 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 167 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S 168 (List.length prefix))) { Types.fst = (Nat.plus inc_pc isize); 169 Types.snd = old_Slength } 169 (Nat.S Nat.O)))))))))))))))) bvSprefixlen { Types.fst = 170 (Nat.plus inc_pc isize); Types.snd = old_Slength } 170 171 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 171 172 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 172 (Nat.S Nat.O)))))))))))))))) 173 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S 174 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 175 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) 176 (List.length prefix)) { Types.fst = inc_pc; Types.snd = 177 new_length } inc_sigma) 173 (Nat.S Nat.O)))))))))))))))) bvprefixlen { Types.fst = inc_pc; 174 Types.snd = new_length } inc_sigma) 178 175 in 179 176 { Types.fst = new_added; Types.snd = { Types.fst = 
src/ASM/PolicyStep.ma
r3039 r3095 1154 1154 program 1155 1155 (λprefix.λx.λtl.λprf.λacc. 1156 let prefixlen ≝ prefix in 1157 let bvprefixlen ≝ bitvector_of_nat ? prefixlen in 1158 let bvSprefixlen ≝ increment … bvprefixlen in 1156 1159 let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in 1157 1160 let 〈label,instr〉 ≝ x in … … 1166 1169 *) 1167 1170 let add_instr ≝ match instr with 1168 [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma (prefix)j)1169  Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma (prefix)c)1170  Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma (prefix)i1171 [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma prefixlen j) 1172  Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma prefixlen c) 1173  Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma prefixlen i 1171 1174  _ ⇒ None ? 1172 1175 ] in 1173 1176 let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in 1174 1177 let old_length ≝ 1175 \snd (bvt_lookup … (bitvector_of_nat ? (prefix))(\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in1178 \snd (bvt_lookup … bvprefixlen (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in 1176 1179 let old_size ≝ instruction_size_jmplen old_length instr in 1177 1180 let 〈new_length, isize〉 ≝ match add_instr with … … 1184 1187 ] in 1185 1188 let old_Slength ≝ 1186 \snd (bvt_lookup … (bitvector_of_nat ? (S (prefix)))(\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in1189 \snd (bvt_lookup … bvSprefixlen (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in 1187 1190 let updated_sigma ≝ 1188 1191 (* we add the new PC to the next position and the new jump length to this one *) 1189 bvt_insert … (bitvector_of_nat ? (S (prefix)))〈inc_pc + isize, old_Slength〉1190 (bvt_insert … (bitvector_of_nat ? (prefix))〈inc_pc, new_length〉 inc_sigma) in1192 bvt_insert … bvSprefixlen 〈inc_pc + isize, old_Slength〉 1193 (bvt_insert … bvprefixlen 〈inc_pc, new_length〉 inc_sigma) in 1191 1194 〈new_added, 〈plus inc_pc isize, updated_sigma〉〉 1192 1195 ) 〈0, 〈0, … … 1247 1250  @not_lt_to_le @ltb_false_to_not_lt @p1 1248 1251 ] 1249 4: lapply (pi2 ?? acc) >p acc inversion inc_pc_sigma 1252 4: 1253 >(?:bvSprefixlen = bitvector_of_nat … (S prefixlen)) 1254 [2: normalize nodelta >increment_zero_bitvector_of_nat_1 <add_bitvector_of_nat %] 1255 lapply (pi2 ?? acc) >p acc inversion inc_pc_sigma 1250 1256 #inc_pc #inc_sigma #Hips normalize nodelta 1251 inversion (bvt_lookup … (bitvector_of_nat ? (prefix))(\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)1257 inversion (bvt_lookup … bvprefixlen (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 1252 1258 #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim 1253 1259 #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.