Changeset 3095 for src/ASM/PolicyStep.ma
 Timestamp:
 Apr 4, 2013, 9:53:30 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.