Changeset 2582


Ignore:
Timestamp:
Jan 15, 2013, 3:58:12 PM (7 years ago)
Author:
garnier
Message:

Some progress on CL to CM.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2578 r2582  
    673673
    674674axiom 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. *)
     677axiom division_u_zero : ∀sz.∀v:BitVector ?. division_u sz (bv_zero ?) v = Some ? (bv_zero ?).
     678
    675679
    676680(* 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  
    336336(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
    337337| 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))))))
    339339| add_case_ip n sz sg ty ⇒
    340     λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp 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))
    341341| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
    342342].
     
    354354| sub_case_pp n1 n2 ty1 ty2 ⇒
    355355    λ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))))))     
    357360    | _ ⇒ Error ? (msg TypeMismatch)
    358361    ]
     
    504507    @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
    505508  | #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: % // ]
    507510  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    508511  ]
     
    792795            [ By_value t ⇒
    793796                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)))),?»
    795798            | By_reference ⇒
    796799(*                do e1' ← region_should_eq r r' ? e1';*)
    797800                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))),?»
    799802            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
    800803            ]
     
    841844          [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)*)
    842845             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))), ?»
    844847      | Tunion _ _ ⇒ translate_addr vars e1
    845848      | _ ⇒ Error ? (msg BadlyTypedAccess)
  • src/Clight/toCminorCorrectness.ma

    r2578 r2582  
    377377     [ 1: destruct (Heq) %2 %1 @refl ]
    378378     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
    380380     | #Hexists %2 %2 @Hexists ]
    381381] qed.
     
    591591qed.
    592592
    593 (*
    594 lemma classify_cmp_inversion :
     593lemma classify_sub_inversion :
    595594  ∀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
     600cases (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 ]
     605qed.
    602606
    603607lemma classify_aop_inversion :
     
    690694%{i'} %{j'} @conj try @conj try @conj try @refl
    691695qed.
     696
     697lemma 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
     706cases 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
     714whd in ⊢ ((??%?) → ?);
     715#H1 destruct
     716cases 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' ]
     725normalize nodelta
     726#H2 destruct
     727try /4 by or_introl, or_intror, conj, refl/
     728%1 %{p} %{p'}
     729cases (if_opt_inversion ???? H2)
     730#Hblocks_eq -H2
     731@(eqb_elim … (sizeof ty1) 0) normalize nodelta
     732#Heq_sizeof destruct #Heq destruct
     733cases (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)
     737qed.
     738
     739
     740lemma 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
     752whd in ⊢ ((??%?) → ?);
     753#H destruct
     754cases 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
     767lemma 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
     776whd in ⊢ ((??%?) → ?); whd in match (classify_sub ??);
     777cases sz cases sg normalize nodelta
     778#H destruct
     779cases v2 in H; normalize nodelta
     780#H1 destruct
     781#H2 destruct #Heq %{sz'} lapply Heq -Heq
     782cases sz' in i'; #i' 
     783whd in match (intsize_eq_elim ???????);
     784cases H1 in H2; #j' normalize nodelta
     785#Heq destruct (Heq)
     786%{i'} %{j'} @conj try @conj try @conj try @refl
     787qed.
     788
    692789
    693790lemma sem_mul_inversion :
     
    10531150qed.
    10541151
    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 *)
     1154lemma 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 ]
     1175whd in match (typ_of_type Tvoid);
     1176#e #f normalize nodelta #Heq destruct
     1177%{sz} %{sg} % try @refl >Heq %
     1178qed.
     1179
     1180 
    10751181
    10761182(* The two following lemmas are just noise. *)
     
    12291335       * [ #Hyp_present_lhs #Hyp_present_rhs
    12301336         | #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 ]
    12321338       whd in match (typeof ?);
    12331339       #Hind_rhs #Hind_lhs
     
    12801386            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    12811387            * #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
    13221443       ]
    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       ]     
    13241610     | 3: (* mul *)
    13251611       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
     
    20032289         whd in match (eval_expr ???????);
    20042290         (* applying the arguments of the induction hypothesis progressively *)
    2005          lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddp I16) cm_expr_ind
     2291         lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddpi I16) cm_expr_ind
    20062292                          (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
    20072293         [ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
  • src/common/FrontEndOps.ma

    r2468 r2582  
    6666  | Ocmpu: ∀sz,sg'.   comparison -> binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint I8 sg') (**r integer unsigned comparison *)
    6767(*  | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') *) (**r float comparison *)
    68   | Oaddp: ∀sz.    binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r add an integer to a pointer *)
     68  | Oaddpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r add an integer to a pointer *)
     69  | Oaddip: ∀sz.   binary_operation  (ASTint sz Signed)  ASTptr                ASTptr              (**r add an integer to a pointer *)
    6970  | Osubpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r subtract int from a pointers *)
    70   | Osubpp: ∀sz.   binary_operation  ASTptr               ASTptr              (ASTint sz Signed)   (**r subtract two pointers *)
     71  | Osubpp: ∀sz.   binary_operation  ASTptr               ASTptr              (ASTint sz Unsigned)   (**r subtract two pointers *)
    7172  | Ocmpp: ∀sg'. comparison → binary_operation ASTptr     ASTptr              (ASTint I8 sg').  (**r compare pointers *)
    7273
     
    213214
    214215(* NB: requires arguments to be presented pointer first. *)
    215 definition ev_addp ≝ λv1,v2: val.
     216definition ev_addpi ≝ λv1,v2: val.
    216217  match v1 with
    217218  [ Vptr ptr1 ⇒ match v2 with
     
    468469  | Ocmpu _ _ c ⇒ ev_cmpu c
    469470(*  | Ocmpf _ _ c ⇒ ev_cmpf c *)
    470   | Oaddp _ ⇒ ev_addp
     471  | Oaddpi _ ⇒ ev_addpi
     472  | Oaddip _ ⇒ (λx,y. ev_addpi y x)
    471473  | Osubpi _ ⇒ ev_subpi
    472474  | Osubpp sz ⇒ ev_subpp sz
     
    504506  whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct // *)
    505507(* pointers *)
    506 | 16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
     508| 16,18: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
    507509  whd in ⊢ (??%? → ?); [ 3,4: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
     510| 17: #sz  #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) % [ 2: #b #o ]
     511  whd in ⊢ (??%? → ?); [ 2: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
    508512| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
    509513  whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?); | ] #E destruct //
Note: See TracChangeset for help on using the changeset viewer.