Changeset 2582 for src/Clight
 Timestamp:
 Jan 15, 2013, 3:58:12 PM (7 years ago)
 Location:
 src/Clight
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2578 r2582 673 673 674 674 axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?). 675 676 (* dividing zero by something eq zero, not the other way around ofc. *) 677 axiom division_u_zero : ∀sz.∀v:BitVector ?. division_u sz (bv_zero ?) v = Some ? (bv_zero ?). 678 675 679 676 680 (* lemma eq_v_to_eq_Z : ∀n. ∀v1,v2:BitVector n. (Z_of_bitvector … v1) = (Z_of_bitvector eq_bv … v1 v2. *) 
src/Clight/toCminor.ma
r2572 r2582 336 336 (* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *) 337 337  add_case_pi n ty sz sg ⇒ 338 λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))338 λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddpi I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty)))))) 339 339  add_case_ip n sz sg ty ⇒ 340 λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd p I16) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))340 λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddip I16) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))) (fix_ptr_type … e2)) 341 341  add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch) 342 342 ]. … … 354 354  sub_case_pp n1 n2 ty1 ty2 ⇒ 355 355 λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with 356 [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2)))))) 356 [ Tint sz sg ⇒ 357 (* XXX we make the constant unsigned to match CL semantics. *) 358 (* OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2)))))) *) 359 OK ? (Op1 ?? (Ocastint I16 Unsigned sz sg) (Op2 ??? (Odivu I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Unsigned (repr ? (sizeof ty2)))))) 357 360  _ ⇒ Error ? (msg TypeMismatch) 358 361 ] … … 504 507 @(typ_equals … E4) E4 E3 % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1) % // ] 505 508  #n #sz #sg #ty0 #E1 #E2 #E3 destruct >E3 #E4 506 @(typ_equals … E4) % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2)% // ]509 @(typ_equals … E4) % [ 2: @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2)  1: % // ] 507 510  #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct 508 511 ] … … 792 795 [ By_value t ⇒ 793 796 OK ? «Mem t (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ? 794 (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off)))),?»797 (Oaddpi …) e1' (Cst ? (Ointconst I16 Signed (repr ? off)))),?» 795 798  By_reference ⇒ 796 799 (* do e1' ← region_should_eq r r' ? e1';*) 797 800 OK ? «Op2 ASTptr (ASTint I16 Signed (* XXX efficiency? *)) ASTptr 798 (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off))),?»801 (Oaddpi …) e1' (Cst ? (Ointconst I16 Signed (repr ? off))),?» 799 802  By_nothing _ ⇒ Error ? (msg BadlyTypedAccess) 800 803 ] … … 841 844 [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)*) 842 845 OK ? «Op2 ASTptr (ASTint I16 Signed (* FIXME inefficient?*)) ASTptr 843 (Oaddp I16) e1' (Cst ? (Ointconst I16 Signed (repr ? off))), ?»846 (Oaddpi I16) e1' (Cst ? (Ointconst I16 Signed (repr ? off))), ?» 844 847  Tunion _ _ ⇒ translate_addr vars e1 845 848  _ ⇒ Error ? (msg BadlyTypedAccess) 
src/Clight/toCminorCorrectness.ma
r2578 r2582 377 377 [ 1: destruct (Heq) %2 %1 @refl ] 378 378 cases (Hind … Hlookup Hexec_alloc) 379 [ @cthulhu (* standard reasoning on positive_maps. check lib. *)379 [ #Hlookup %1 <(lookup_add_miss SymbolTag ? init_env ?? blo (sym_neq ??? Hneq)) @Hlookup 380 380  #Hexists %2 %2 @Hexists ] 381 381 ] qed. … … 591 591 qed. 592 592 593 (* 594 lemma classify_cmp_inversion : 593 lemma classify_sub_inversion : 595 594 ∀ty1,ty2. 596 if_type_eq ty1 ty2 (λty1, ty2. classify_cmp_cases ty1 ty2) 597 ((∃sz,sg. ty1 = Tint sz sg ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_ii sz sg) ∨ 598 (∃ty'. ty1 = Tpointer ty' ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_pp (None ?) ty') ∨ 599 (∃ty',n'. ty1 = Tarray ty' n' ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_pp (Some ? n') ty') ∨ 600 (classify_cmp ty1 ty2 = cmp_default …) 601 *) 595 (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_ii sz sg) ∨ 596 (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_pi n ty' sz sg) ∨ 597 (∃ty1',ty2',n1,n2. ty1 = ptr_type ty1' n1 ∧ ty2 = ptr_type ty2' n2 ∧ classify_sub ty1 ty2 ≃ sub_case_pp n1 n2 ty1' ty2') ∨ 598 (classify_sub ty1 ty2 = sub_default ty1 ty2). 599 #ty1 #ty2 600 cases (classify_sub ty1 ty2) 601 [ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq 602  #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq 603  #n1 #n2 #t1 #t2 %1 %2 %{t1} %{t2} %{n1} %{n2} @conj try @conj try @refl @refl_jmeq 604  #tya #tyb %2 @refl ] 605 qed. 602 606 603 607 lemma classify_aop_inversion : … … 690 694 %{i'} %{j'} @conj try @conj try @conj try @refl 691 695 qed. 696 697 lemma sem_sub_pp_inversion : 698 ∀ty1,ty2,n1,n2. 699 ∀v1,v2,res. 700 sem_sub v1 (ptr_type ty1 n1) v2 (ptr_type ty2 n2) = Some ? res → 701 (∃p1,p2,i. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧ pblock p1 = pblock p2 ∧ 702 division_u ? (sub_offset ? (poff p1) (poff p2)) (repr (sizeof ty1)) = Some ? i ∧ 703 res = Vint I32 i) ∨ 704 (v1 = Vnull ∧ v2 = Vnull ∧ res = Vint I32 (zero ?)). 705 #ty1 #ty2 #n1 #n2 706 cases n1 cases n2 707 [  #n1  #n2  #n2 #n1 ] 708 * 709 [  #sz #i   #p 710   #sz #i   #p 711   #sz #i   #p 712   #sz #i   #p ] 713 #v2 #res 714 whd in ⊢ ((??%?) → ?); 715 #H1 destruct 716 cases v2 in H1; 717 [  #sz' #i'   #p' 718   #sz' #i'   #p' 719   #sz' #i'   #p' 720   #sz' #i'   #p' 721   #sz' #i'   #p' 722   #sz' #i'   #p' 723   #sz' #i'   #p' 724   #sz' #i'   #p' ] 725 normalize nodelta 726 #H2 destruct 727 try /4 by or_introl, or_intror, conj, refl/ 728 %1 %{p} %{p'} 729 cases (if_opt_inversion ???? H2) 730 #Hblocks_eq H2 731 @(eqb_elim … (sizeof ty1) 0) normalize nodelta 732 #Heq_sizeof destruct #Heq destruct 733 cases (division_u ???) in Heq; normalize nodelta 734 #H3 destruct #H4 destruct 735 %{H3} try @conj try @conj try @conj try @conj try @refl 736 @(eq_block_to_refl … Hblocks_eq) 737 qed. 738 739 740 lemma sem_sub_pi_inversion : 741 ∀sz,sg,ty',optlen. 742 ∀v1,v2,res. 743 sem_sub v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res → 744 ∃sz',i. v2 = Vint sz' i ∧ 745 ((∃p. v1 = Vptr p ∧ res = Vptr (neg_shift_pointer_n ? p (sizeof ty') sg i)) ∨ 746 (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)). 747 #tsz #tsg #ty' * [  #n ] 748 * 749 [  #sz' #i'   #p' 750   #sz' #i'   #p' ] 751 #v2 #res 752 whd in ⊢ ((??%?) → ?); 753 #H destruct 754 cases v2 in H; normalize nodelta 755 [  #sz2' #i2'   #p2'   #sz2' #i2'   #p2'   #sz2' #i2'   #p2'   #sz2' #i2'   #p2' ] 756 #H destruct 757 [ 2,4: %{sz2'} %{i2'} @conj try @refl %1 758 %{p'} @conj try @refl 759  *: lapply H H 760 @(eq_bv_elim … i2' (zero ?)) normalize nodelta 761 #Hi #Heq destruct (Heq) 762 %{sz2'} %{(zero ?)} @conj destruct try @refl 763 %2 @conj try @conj try @refl 764 ] qed. 765 766 767 lemma sem_sub_ii_inversion : 768 ∀sz,sg. 769 ∀v1,v2,res. 770 sem_sub v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res → 771 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 772 res = Vint sz' (subtraction (bitsize_of_intsize sz') i1 i2). 773 #sz #sg * 774 [  #sz' #i'   #p' ] 775 #v2 #res 776 whd in ⊢ ((??%?) → ?); whd in match (classify_sub ??); 777 cases sz cases sg normalize nodelta 778 #H destruct 779 cases v2 in H; normalize nodelta 780 #H1 destruct 781 #H2 destruct #Heq %{sz'} lapply Heq Heq 782 cases sz' in i'; #i' 783 whd in match (intsize_eq_elim ???????); 784 cases H1 in H2; #j' normalize nodelta 785 #Heq destruct (Heq) 786 %{i'} %{j'} @conj try @conj try @conj try @refl 787 qed. 788 692 789 693 790 lemma sem_mul_inversion : … … 1053 1150 qed. 1054 1151 1055 (* 1056 lemma pointer_translation_cmp_offset : 1057 ∀E,p1,p2,p1',p2',op. 1058 pblock p1 = pblock p2 → 1059 pointer_translation p1 E = Some ? p1' → 1060 pointer_translation p2 E = Some ? p2' → 1061 cmp_offset op (poff p1) (poff p2) = cmp_offset op (poff p1') (poff p2'). 1062 #E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2' #op #Heq destruct 1063 whd in ⊢ ((??%?) → (??%?) → ?); 1064 cases (E b2) normalize nodelta 1065 [ #H destruct ] 1066 * #bx #ox normalize nodelta 1067 #Heq1 #Heq2 destruct cases op 1068 [ @sym_eq @eq_offset_translation 1069  @sym_eq @neq_offset_translation 1070  @cthulhu (* !!!! TODO !!!! *) 1071  @cthulhu (* !!!! TODO !!!! *) 1072  @cthulhu (* !!!! TODO !!!! *) 1073  @cthulhu (* !!!! TODO !!!! *) 1074 ] qed. *) 1152 1153 (* avoid a case analysis on type inside of a big proof *) 1154 lemma match_type_inversion_aux : ∀ty,e,f. 1155 match ty in type return λty':type.(res (expr (typ_of_type ty'))) with 1156 [Tvoid⇒Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch) 1157 Tint (sz:intsize) (sg:signedness)⇒ f sz sg 1158 Tpointer (x:type)⇒ 1159 Error (expr (typ_of_type (Tpointer x))) (msg TypeMismatch) 1160 Tarray (x:type) (y:ℕ)⇒ 1161 Error (expr (typ_of_type (Tarray x y))) (msg TypeMismatch) 1162 Tfunction (x:typelist) (y:type)⇒ 1163 Error (expr (typ_of_type (Tfunction x y))) (msg TypeMismatch) 1164 Tstruct (x:ident) (y:fieldlist)⇒ 1165 Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch) 1166 Tunion (x:ident) (y:fieldlist)⇒ 1167 Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch) 1168 Tcomp_ptr (x:ident)⇒ 1169 Error (expr (typ_of_type (Tcomp_ptr x))) (msg TypeMismatch)] 1170 = OK ? e → 1171 ∃sz,sg. ty = Tint sz sg ∧ (f sz sg ≃ OK ? e). 1172 * 1173 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1174  #structname #fieldspec  #unionname #fieldspec  #id ] 1175 whd in match (typ_of_type Tvoid); 1176 #e #f normalize nodelta #Heq destruct 1177 %{sz} %{sg} % try @refl >Heq % 1178 qed. 1179 1180 1075 1181 1076 1182 (* The two following lemmas are just noise. *) … … 1229 1335 * [ #Hyp_present_lhs #Hyp_present_rhs 1230 1336  #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst 1231  #Hyp_present_rhs * #Hyp_present_lhs #Hyp_present_cst]1337  * #Hyp_present_lhs #Hyp_present_cst #Hyp_present_rhs ] 1232 1338 whd in match (typeof ?); 1233 1339 #Hind_rhs #Hind_lhs … … 1280 1386 lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1281 1387 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1282 [ 1: lapply (sem_add_pi_inversion … Hsem_binary_translated) 1283 * #cm_vsz * #cm_rhs_v * #Hcm_rhs * 1284 [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr 1285  * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ] 1286 destruct 1287 whd in match (eval_unop ????); 1288 @(match sg 1289 return λs. sg = s → ? 1290 with 1291 [ Unsigned ⇒ λHsg. ? 1292  Signed ⇒ λHsg. ? 1293 ] (refl ??)) normalize nodelta 1294 whd in match (eval_binop ???????); 1295 whd in match (m_bind ?????); 1296 [ 1: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr 1297 (short_multiplication (bitsize_of_intsize I16) 1298 (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v) 1299 (repr I16 (sizeof ty')))))} 1300  2: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr 1301 (short_multiplication (bitsize_of_intsize I16) 1302 (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v) 1303 (repr I16 (sizeof ty')))))} ] 1304 [ 1,2: @conj whd in match (E0); whd in match (Eapp trace_rhs ?); 1305 >(append_nil … trace_rhs) try @refl 1306 @(value_eq_triangle_diagram … Hvalue_eq_res) 1307 whd in match (shift_pointer_n ????); 1308 whd in match (shift_offset_n ????); 1309 >commutative_short_multiplication 1310 whd in match (shift_pointer ???); 1311 whd in match (shift_offset ???); 1312 @cthulhu (* cf problem description at top of lemma. *) 1313  3: >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) 1314 >(short_multiplication_zero 16 (repr I16 (sizeof ty'))) 1315 >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption 1316 normalize >append_nil try @refl 1317  4: >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) 1318 >(short_multiplication_zero 16 (repr I16 (sizeof ty'))) 1319 >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption 1320 normalize >append_nil try @refl ] 1321  2: (* integer/pointer add: symmetric to the case above. *) @cthulhu ] 1388 (* >> *) 1389 [ lapply (sem_add_pi_inversion … Hsem_binary_translated) 1390 * #cm_vsz * #cm_rhs_v * #Hcm_rhs * 1391 [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr 1392  * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ] 1393  lapply (sem_add_ip_inversion … Hsem_binary_translated) 1394 * #cm_vsz * #cm_lhs_v * #Hcm_lhs * 1395 [ * #rhs_ptr * #Hcm_rhs_ptr #Hcm_val_shptr 1396  * * #rhs_null #Hcm_lhs_zero #Hcm_val_null ] 1397 ] 1398 destruct 1399 whd in match (eval_unop ????); 1400 @(match sg 1401 return λs. sg = s → ? 1402 with 1403 [ Unsigned ⇒ λHsg. ? 1404  Signed ⇒ λHsg. ? 1405 ] (refl ??)) normalize nodelta 1406 whd in match (eval_binop ???????); 1407 whd in match (m_bind ?????); 1408 [ 1: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr 1409 (short_multiplication (bitsize_of_intsize I16) 1410 (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v) 1411 (repr I16 (sizeof ty')))))} 1412  2: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr 1413 (short_multiplication (bitsize_of_intsize I16) 1414 (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v) 1415 (repr I16 (sizeof ty')))))} 1416  5: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr 1417 (short_multiplication (bitsize_of_intsize I16) 1418 (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v) 1419 (repr I16 (sizeof ty')))))} 1420  6: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr 1421 (short_multiplication (bitsize_of_intsize I16) 1422 (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v) 1423 (repr I16 (sizeof ty')))))} 1424 ] 1425 [ 1,2,3,4: @conj whd in match (E0); 1426 whd in match (Eapp trace_rhs ?); 1427 whd in match (Eapp trace_lhs ?); 1428 >(append_nil … trace_rhs) try @refl 1429 >(append_nil … trace_lhs) try @refl 1430 @(value_eq_triangle_diagram … Hvalue_eq_res) 1431 whd in match (shift_pointer_n ?????); 1432 whd in match (shift_offset_n ?????); 1433 >Hsg normalize nodelta 1434 >commutative_short_multiplication 1435 whd in match (shift_pointer ???); 1436 whd in match (shift_offset ???); 1437 >sign_ext_same_size @refl 1438  5,7: >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) 1439  6,8: >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) ] 1440 >(short_multiplication_zero 16 (repr I16 (sizeof ty'))) 1441 >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption 1442 normalize >append_nil try @refl 1322 1443 ] 1323  2: (* subtraction cases: identical to add *) @cthulhu 1444  2: (* subtraction cases: not quite identical to add. *) 1445 lapply (classify_sub_inversion (typeof e1) (typeof e2)) 1446 * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] 1447 lapply e' e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e' 1448 * [ 1: * ] 1449 [ 1: * #sz * #sg * * 1450  2: * #optlen * #ty' * #sz * #sg * * 1451  3: * #t1 * #t2 * #n1 * #n2 * * ] 1452 whd in match (typeof ?) in ⊢ (% → % → ?); 1453 #Htypeof_e1 #Htypeof_e2 1454 >Htypeof_e1 >Htypeof_e2 1455 #Hclassify 1456 lapply (jmeq_to_eq ??? Hclassify) Hclassify #Hclassify >Hclassify 1457 normalize nodelta 1458 whd in match (typeof ?) in ⊢ (% → % → %); 1459 whd in match (typ_of_type (Tint ??)); 1460 #lhs #rhs 1461 [ 1: #Htyp_should_eq cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq) 1462 Htyp_should_eq 1463  2: #Htyp_should_eq cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq) 1464 Htyp_should_eq 1465  3: #Haux cases (match_type_inversion_aux … Haux) #ty_sz * #ty_sg * Haux 1466 #Hty_eq #Heq_aux destruct (Hty_eq) lapply (jmeq_to_eq ??? Heq_aux) Heq_aux 1467 #Heq_e' destruct (Heq_e') ] 1468 [ 1,2: #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') Heq_e' #Heq_e' 1469 <Heq_e' Heq_e'  ] 1470 #Hexec 1471 #Hexpr_vars_rhs #Hexpr_vars_lhs 1472 #Htranslate_rhs #Htranslate_lhs 1473 * [ #Hyp_present_lhs #Hyp_present_rhs 1474  #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst 1475  * #Hyp_present_lhs #Hyp_present_rhs #Hyp_present_cst ] 1476 whd in match (typeof ?); 1477 #Hind_rhs #Hind_lhs 1478 cases (bind_inversion ????? Hexec) Hexec 1479 * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec 1480 cases (bind_inversion ????? Hexec) Hexec 1481 * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec 1482 cases (bind_inversion ????? Hexec) Hexec 1483 #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 1484 lapply (opt_to_res_inversion ???? Hsem) Hsem 1485 whd in match (typeof ?); whd in match (typeof ?); 1486 #Hsem_binary 1487 whd in match (eval_expr ???????); 1488 whd in match (proj1 ???); 1489 whd in match (eval_expr ???????); 1490 whd in match (eval_expr ???????); 1491 whd in match (proj1 ???); 1492 [ 1: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs) 1493  2,3: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ] 1494 * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs Hind_lhs 1495 [ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs) 1496  3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ] 1497 * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs Hind_rhs 1498 [ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) Heval_lhs #Heval_lhs ] 1499 [ 1,2: >Heval_lhs normalize nodelta 1500 whd in match (eval_expr ???????); 1501 whd in match (eval_expr ???????); 1502 [ >(eval_expr_rewrite_aux … Heval_rhs) 1503  >Heval_rhs ] 1504 whd in match (m_bind ?????); 1505 normalize nodelta 1506  3: >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta 1507 whd in match (eval_expr ???????); 1508 whd in match (eval_expr ???????); 1509 >Heval_rhs normalize nodelta 1510 whd in match (eval_unop ????); 1511 ] 1512 [ 1: (* ptr/ptr sub *) 1513 whd in Hsem_binary:(??%?); 1514 lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1515 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1516 lapply (sem_sub_pp_inversion … Hsem_binary_translated) * 1517 [ (* regular pointers case *) 1518 * #lhs_ptr * #rhs_ptr * #resulting_offset * * * * 1519 #Hcm_lhs #Hcm_rhs #Hblocks_eq #Hoffset_eq #Hcm_val_eq 1520 whd in match (eval_binop ???????); 1521 >Hcm_lhs >Hcm_rhs normalize nodelta >Hblocks_eq >eq_block_b_b 1522 normalize nodelta 1523 whd in match (eval_expr ???????); 1524 whd in match (m_bind ?????); 1525 whd in match (eval_binop ???????); 1526 (* size mismatch between CL and CM. TODO *) 1527 @cthulhu 1528  (* null pointers case *) 1529 * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct 1530 whd in match (eval_binop ???????); normalize nodelta 1531 whd in match (eval_expr ???????); 1532 whd in match (m_bind ?????); 1533 whd in match (eval_binop ???????); normalize nodelta 1534 >division_u_zero normalize nodelta 1535 whd in match (eval_unop ????); 1536 whd in match (opt_to_res ???); 1537 whd in match (m_bind ?????); 1538 whd in match (pred_size_intsize ?); 1539 %{(zero_ext ty_sz (Vint I16 (zero (S (7+1*8)))))} @conj 1540 [ whd in match (Eapp ??); whd in match E0; >append_nil try @refl ] 1541 whd in Hsem_binary_translated:(??%?); 1542 normalize nodelta in Hsem_binary_translated:(??%?); 1543 lapply Hsem_binary_translated; Hsem_binary_translated; 1544 cases n1 cases n2 1545 [  2,3: #n  #n1 #n2 ] normalize nodelta 1546 #Heq destruct (Heq) 1547 (* size mismatch between CL and CM. TODO *) 1548 @cthulhu 1549 ] 1550  2: (* int/int sub *) 1551 whd in match (eval_binop ???????); 1552 whd in Hsem_binary:(??%?); 1553 lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1554 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1555 cases (sem_sub_ii_inversion … Hsem_binary_translated) 1556 #cm_vsz * #cm_lhs_v * #cm_rhs_v * * 1557 #Hcm_lhs #Hcm_rhs #Hcm_val 1558 destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta 1559 >intsize_eq_elim_true normalize nodelta 1560 %{(Vint cm_vsz (subtraction (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))} 1561 @conj try @refl lapply Hsem_binary_translated 1562 whd in ⊢ ((??%?) → ?); normalize nodelta whd in match (classify_sub ??); 1563 >type_eq_dec_true normalize nodelta 1564 >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res 1565  3: (* ptr/int sub *) 1566 whd in Hsem_binary:(??%?); 1567 lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) 1568 * #cm_val * #Hsem_binary_translated #Hvalue_eq_res 1569 lapply (sem_sub_pi_inversion … Hsem_binary_translated) Hsem_binary_translated 1570 * #cm_vsz * #cm_rhs_v * #Hcm_rhs * 1571 [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr 1572  * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ] 1573 whd in match (eval_unop ????); 1574 Heval_lhs Heval_rhs destruct 1575 whd in match (proj2 ???); 1576 @(match sg 1577 return λs. sg = s → ? 1578 with 1579 [ Unsigned ⇒ λHsg. ? 1580  Signed ⇒ λHsg. ? 1581 ] (refl ??)) normalize nodelta 1582 whd in match (eval_expr ???????); 1583 whd in match (m_bind ?????); 1584 whd in match (eval_binop ???????); 1585 [ 1,2: 1586 %{(Vptr 1587 (neg_shift_pointer_n (bitsize_of_intsize cm_vsz) lhs_ptr (sizeof ty') sg 1588 cm_rhs_v))} try @conj try assumption 1589 (* TODO size mismatch (?) or insert zero/sign_ext in semantics *) 1590 (* [ 1,2,3,4: @conj whd in match (E0); 1591 whd in match (Eapp trace_rhs ?); 1592 whd in match (Eapp trace_lhs ?); 1593 >(append_nil … trace_rhs) try @refl 1594 >(append_nil … trace_lhs) try @refl 1595 @(value_eq_triangle_diagram … Hvalue_eq_res) 1596 whd in match (shift_pointer_n ?????); 1597 whd in match (shift_offset_n ?????); 1598 >Hsg normalize nodelta 1599 >commutative_short_multiplication 1600 whd in match (shift_pointer ???); 1601 whd in match (shift_offset ???); 1602 >sign_ext_same_size @refl *) 1603 @cthulhu ] 1604 [ >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) 1605  >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) ] 1606 >(short_multiplication_zero 16 (repr I16 (sizeof ty'))) 1607 >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption 1608 normalize >append_nil try @refl 1609 ] 1324 1610  3: (* mul *) 1325 1611 lapply (classify_aop_inversion (typeof e1) (typeof e2)) * … … 2003 2289 whd in match (eval_expr ???????); 2004 2290 (* applying the arguments of the induction hypothesis progressively *) 2005 lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddp I16) cm_expr_ind2291 lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddpi I16) cm_expr_ind 2006 2292 (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?) 2007 2293 [ 1,3,5,7,9: whd @conj try assumption whd @I ] Hind #Hind
Note: See TracChangeset
for help on using the changeset viewer.