Changeset 2030


Ignore:
Timestamp:
Jun 8, 2012, 1:44:31 PM (5 years ago)
Author:
garnier
Message:

Cast simplification was too conservative, now reasonably aggressive.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2019 r2030  
    55include "Clight/Cexec.ma".
    66include "Clight/casts.ma".
     7include "Clight/CexecSound.ma".
     8
    79
    810(* include "ASM/AssemblyProof.ma". *) (* I had to manually copy some of the lemmas in this file, including an axiom ... *)
     
    139141].
    140142
     143lemma size_lt_to_le : ∀sz1,sz2. size_lt sz1 sz2 → size_le sz1 sz2.
     144#sz1 #sz2 elim sz1 elim sz2 normalize // qed.
     145
    141146lemma size_lt_dec : ∀sz1,sz2. size_lt sz1 sz2 + (¬ (size_lt sz1 sz2)).
    142147* * normalize /2/ /3/
     
    186191       | 2: #Hsg_neq #_ %2 destruct /2/ ]
    187192     ]
    188 ] qed.     
    189 
     193] qed.
    190194
    191195(* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an
    192196 * integer value smaller but containing the same stuff than [r2] then all is well.
    193197 * If the first evaluation is erroneous, we don't care about anything else. *)
    194 definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res (val×trace).
     198definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res(val×trace).
    195199match r1 with
    196200[ OK res1 ⇒
     201  let 〈val1, tr1〉 ≝ res1 in
     202  ∀v1. val1 = Vint src_sz v1 → 
    197203  match r2 with
    198   [ OK res2 ⇒
    199     let 〈v1, tr1〉 ≝ res1 in
    200     let 〈v2, tr2〉 ≝ res2 in
    201     match v1 with
    202     [ Vint sz1 v1 ⇒
    203        match v2 with
    204        [ Vint sz2 v2 ⇒
    205          match sz_eq_dec sz1 src_sz with
    206          [ inl Hsrc_eq ⇒
    207             match sz_eq_dec sz2 dst_sz with
    208             [ inl Hdst_eq ⇒
    209                 v2 = cast_int_int sz1 sg sz2 v1
    210                 ∧ tr1 = tr2
    211                 ∧ size_le dst_sz src_sz
    212             | inr _ ⇒ False ]
    213          | inr _ ⇒ False ]
    214        | _ ⇒ False ]
    215     | _ ⇒ False ]
     204  [ OK res2 ⇒
     205    let 〈val2, tr2〉 ≝ res2 in
     206    ∃v2. (val2 = Vint dst_sz v2 ∧
     207          v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz)   
    216208  | _ ⇒ False ]
    217 | Error errmsg1 ⇒ True (* Simulation ... *)
    218 (*  match r2 with
    219   [ OK _ ⇒ False
    220   | Error errmsg2 ⇒ True (* Note that the two expressions may fail for different reasons ... Too lax maybe ? *)
    221   ] *)
     209| Error errmsg1 ⇒ True
    222210].
    223 
    224 (* Inversion on smaller_integer_val *)
    225 lemma smaller_integer_val_spec : ∀src_sz,dst_sz,sg,val1,val2,tr1,tr2.
    226     smaller_integer_val src_sz dst_sz sg (OK ? 〈val1, tr1〉) (OK ? 〈val2, tr2〉) →
    227     ∃v1,v2. val1 = Vint src_sz v1 ∧ val2 = Vint dst_sz v2 ∧
    228     v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz.
    229 #src_sz #dst_sz #sg #val1 #val2 #tr1 #tr2
    230 whd in ⊢ (% → ?);
    231 elim val1 normalize nodelta
    232 [ 1: #Hcontr @(False_ind … Hcontr) | 3,4,5: #foo #Hcontr @(False_ind … Hcontr)
    233 | 2: #size1 #int1 cases val2
    234      [ 1: #Hcontr @(False_ind … Hcontr) | 3,4,5: #foo #Hcontr @(False_ind … Hcontr)
    235      | 2: #size2 #int2 normalize nodelta
    236           cases (sz_eq_dec size1 src_sz)
    237           cases (sz_eq_dec size2 dst_sz)
    238           [ 2,3,4: #Hneq #Heq #Hcontr @(False_ind … Hcontr)
    239           | 1: #Heq1 #Heq2 * * #Hcast #Htrace #H destruct
    240                @(ex_intro … int1) @(ex_intro … (cast_int_int src_sz sg dst_sz int1))
    241                try @conj try @conj try @conj try @conj try @conj try @conj //
    242           ]
    243      ]
    244 ] qed.
    245211
    246212(* Simulation relation used for expression evaluation. *)
     
    265231     simplify_inv ge en m e1 e2 target_sz target_sg true.
    266232     
     233(* Invariant of simplify_inside *)     
    267234definition conservation ≝ λe,result:expr.
    268235∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result)
     
    731698     lapply (Hind ? tl) #H
    732699     whd in match (two_complement_negation ??) in H;
    733 (* trying to reduce add_with_carries *)     
     700     (* trying to reduce add_with_carries *)     
    734701     normalize in match (S m'+n);
    735702     whd in match (zero ?) in ⊢ (???%);
     
    737704     whd in match (negation_bv ??) in ⊢ (???%);
    738705     >add_with_carries_unfold in ⊢ (???%);
    739 (*     >truncate_tail *)
    740706     normalize in ⊢ (???%);
    741707     cases hd normalize nodelta
     
    803769     ]
    804770] qed.
    805      
     771
     772lemma simplify_int_success_lt : ∀sz,sg,sz',sg',i,i'. (simplify_int sz sz' sg sg' i=Some (bvint sz') i') → size_le  sz' sz.
     773* #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed.
     774
     775lemma smaller_integer_val_identity : ∀sz,sg,x.
     776     smaller_integer_val sz sz sg x x.
     777#sz #sg *
     778[ 2: #error //
     779| 1: * #val #trace whd in match (smaller_integer_val ?????);
     780     #v1 #Hval %{v1} @conj try @conj try @conj //
     781     elim sz //
     782] qed.     
     783
     784(* Inversion on exec_cast *)
     785lemma exec_cast_inv : ∀castee_val,src_sz,src_sg,cast_sz,cast_sg,m,result.
     786                         exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg) = OK ? result →
     787                         ∃i. castee_val = Vint src_sz i ∧ result = Vint cast_sz (cast_int_int src_sz src_sg cast_sz i).
     788#castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result
     789elim castee_val
     790[ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     791[ 2: | *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ]
     792whd in ⊢ ((??%?) → ?);
     793cases (sz_eq_dec sz' src_sz)
     794[ 1: #Heq destruct >intsize_eq_elim_true normalize nodelta #Heq destruct
     795     %{i}  /2/
     796| 2: #Hneq >intsize_eq_elim_false; try assumption #H destruct ]
     797qed.
     798
     799
     800(* Lemmas related to the Ebinop case *)
     801
    806802lemma classify_add_int : ∀sz,sg. classify_add (Tint sz sg) (Tint sz sg) = add_case_ii sz sg.
    807803* * // qed.
     
    812808lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true.
    813809* * normalize #H @conj // qed.
    814 
    815 lemma simplify_int_success_lt : ∀sz,sg,sz',sg',i,i'. (simplify_int sz sz' sg sg' i=Some (bvint sz') i') → size_le  sz' sz.
    816 * #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed.
    817810
    818811(* Operations where it is safe to use a smaller integer type on the assumption
     
    820813definition binop_simplifiable ≝
    821814λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ].
     815
     816(* Inversion principle for integer addition *)
     817lemma iadd_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
     818                                    ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (addition_n (bitsize_of_intsize dsz) i1 i2)).
     819#sz #sg #v1 #v2 #m #r
     820elim v1
     821[ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     822whd in ⊢ ((??%?) → ?); normalize nodelta
     823>classify_add_int normalize nodelta #H destruct
     824elim v2 in H;
     825[ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     826whd in ⊢ ((??%?) → ?); #H destruct
     827elim (sz_eq_dec sz' sz'')
     828[ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
     829| 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
     830] qed.
     831
     832(* Inversion principle for integer subtraction. *)
     833lemma isub_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
     834                                    ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)).
     835#sz #sg #v1 #v2 #m #r
     836elim v1
     837[ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     838whd in ⊢ ((??%?) → ?); normalize nodelta
     839>classify_sub_int normalize nodelta #H destruct
     840elim v2 in H;
     841[ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     842whd in ⊢ ((??%?) → ?); #H destruct
     843elim (sz_eq_dec sz' sz'')
     844[ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
     845| 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
     846] qed.
     847
     848definition is_int : val → Prop ≝
     849λv.
     850match v with
     851[ Vint _ _ ⇒ True
     852| _ ⇒ False ].
     853
     854(* "negative" (in the sense of ¬ Some) inversion principle for integer addition *)
     855lemma neg_iadd_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
     856                                        ¬ (is_int v1) ∨ ¬ (is_int v2) ∨
     857                                        ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
     858#sz #sg #v1 #v2 #m
     859elim v1
     860[ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     861[ 2: | *: #_ %1 %1 % #H @H ]
     862elim v2
     863[ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     864[ 2: | *: #_ %1 %2 % #H @H ]
     865whd in ⊢ ((??%?) → ?); normalize nodelta
     866>classify_add_int normalize nodelta
     867elim (sz_eq_dec sz' sz'')
     868[ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd)
     869| 2: #Hneq >intsize_eq_elim_false try assumption #_
     870     %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj //
     871] qed.
     872
     873(* "negative" inversion principle for integer subtraction *)
     874lemma neg_isub_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
     875                                        ¬ (is_int v1) ∨ ¬ (is_int v2) ∨
     876                                        ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
     877#sz #sg #v1 #v2 #m
     878elim v1
     879[ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     880[ 2: | *: #_ %1 %1 % #H @H ]
     881elim v2
     882[ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     883[ 2: | *: #_ %1 %2 % #H @H ]
     884whd in ⊢ ((??%?) → ?); normalize nodelta
     885>classify_sub_int normalize nodelta
     886elim (sz_eq_dec sz' sz'')
     887[ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd)
     888| 2: #Hneq >intsize_eq_elim_false try assumption #_
     889     %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj //
     890] qed.
     891
     892
     893lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m.
     894   ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?.
     895#op #sz #sg #v1 #v2 #m #H
     896elim op normalize in match (binop_simplifiable ?); #H destruct
     897elim v1 in H;
     898[ 1,6: | 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,8: #f | 4,9: #r | 5,10: #ptr ]
     899#_
     900whd in match (sem_binary_operation ??????); normalize nodelta
     901>classify_add_int normalize nodelta //
     902>classify_sub_int normalize nodelta //
     903qed.
    822904
    823905notation > "hvbox('let' «ident x,ident y» 'as' ident E ≝ t 'in' s)"
     
    833915       ] (refl ? $t)
    834916      }.
    835                  
    836                        
     917
    837918(* This function will make your eyes bleed. You've been warned.
    838919 * Implements a correct-by-construction version of Brian's original cast-removal code. Does so by
     
    10161097      ]               
    10171098  | Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?»
    1018   | Evar id        ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?»
     1099(* | Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *)
     1100  (* In order for the simplification function to be less dymp, we would have to use this line, which would in fact
     1101     require to alter the semantics of [load_value_of_type].  *)
     1102  | Evar id        ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?»
    10191103  | Esizeof t      ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?»
    10201104  ] (refl ? ed)
     
    10851169     cases (exec_expr ge en m e) #res
    10861170     try (@(SimOk ???) //)
    1087 | 13,14: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res
    1088      try (@(SimOk ???) //)
    10891171| 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct /by refl/
     1172(*
    10901173     whd in match (exec_expr ????); >eq_intsize_identity whd
    10911174     >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ]
     1175*)     
    10921176| 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) / by refl/
    10931177     whd in match (exec_expr ????);
    10941178     whd in match (exec_expr ????);
    10951179     >eq_intsize_identity >eq_intsize_identity whd
    1096      >sz_eq_identity >sz_eq_identity whd @conj try @conj try @refl     
     1180     #v1 #Heq destruct (Heq) %{i'} try @conj try @conj try @conj //
    10971181     [ 1: @(simplify_int_implements_cast … Hsimpl_eq)
    10981182     | 2: @(simplify_int_success_lt … Hsimpl_eq) ]
     1183| 13: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res
     1184      try (@(SimOk ???) //)
     1185| 14: elim (type_eq_dec ty (Tint target_sz target_sg))
     1186      [ 1: #Heq >Heq >type_eq_identity @(Inv_coerce_ok ??????? target_sz target_sg)
     1187           destruct
     1188           [ 1,2: //
     1189           | 3: @smaller_integer_val_identity ]
     1190      | 2: #Hneq >(type_neq_not_identity … Hneq) %1 // destruct
     1191           @(SimOk ???) //
     1192      ]
    10991193| 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    11001194    [ 1: (* Proving preservation of the semantics for expressions. *)
     
    12141308                | 3: whd in match (exec_expr ??? (Expr ??));
    12151309                     whd in match (exec_expr ??? (Expr ??));
     1310                     (* Tidy up the type equations *)
     1311                     >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Heq destruct
     1312                     lapply Hsmaller_rhs lapply Hsmaller_lhs
     1313                     generalize in match rhs_src_sz; #src_sz
     1314                     generalize in match rhs_src_sg; #src_sg
     1315                     -Hsmaller_lhs -Hsmaller_rhs -Htype_lhs -Htype_rhs -Hinv_lhs -Hinv_rhs
     1316                     >Htype_lhs1 >Htype_rhs1 -Htype_lhs1 -Htype_rhs1
    12161317                     (* Enumerate all the cases for the evaluation of the source expressions ... *)
    1217                      cases (exec_expr ge en m lhs) in Hsmaller_lhs;
    1218                      [ 2: #error //
    1219                      | 1: * #val_lhs #trace_lhs normalize nodelta cases (exec_expr ge en m lhs1)
    1220                           [ 2: #error #H @(False_ind … H)
    1221                           | 1: * #val_lhs1 #trace_lhs1 #Hsmaller_lhs
    1222                                elim (smaller_integer_val_spec … Hsmaller_lhs)
    1223                                #lhs_int * #lhs1_int * * * * #Hval_lhs #Hval_lhs1 #Hlhs_cast #Hlhs_trace #Hlhs_size
    1224                                cases (exec_expr ge en m rhs) in Hsmaller_rhs;
    1225                                [ 2: #error //
    1226                                | 1: * #val_rhs #trace_rhs normalize nodelta cases (exec_expr ge en m rhs1)
    1227                                     [ 2: #error #H @(False_ind … H)
    1228                                     | 1: * #val_rhs1 #trace_rhs1 #Hsmaller_rhs
    1229                                          elim (smaller_integer_val_spec … Hsmaller_rhs)
    1230                                          #rhs_int * #rhs1_int * * * * #Hval_rhs #Hval_rhs1 #Hrhs_cast #Hrhs_trace #Hrhs_size
    1231                                          whd in match (m_bind ?????);
    1232                                          whd in match (m_bind ?????);
    1233                                          <Htylhs_eq_tyrhs >Htype_lhs
    1234                                          >Htype_lhs1 >Htype_rhs1
    1235                                          cut (lhs_src_sz = rhs_src_sz ∧ lhs_src_sg = rhs_src_sg)
    1236                                          [ 1: >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Hty_eq destruct (Hty_eq)
    1237                                                @conj // ]
    1238                                          * #Hsrc_sz_eq #Hsrc_sg_eq
    1239                                          cases op in Hop_simplifiable_eq;
    1240                                          normalize in match (binop_simplifiable ?);
    1241                                          [ 3,4,5,6,7,8,9,10,11,12,13,14,15,16: #H destruct (H)
    1242                                          | 1: #_ (* addition case *)
    1243                                              >Hval_lhs >Hval_rhs destruct                                               
    1244                                              whd in match (sem_binary_operation Oadd ?????);
    1245                                              whd in match (sem_binary_operation Oadd ?????); normalize nodelta
    1246                                              >classify_add_int >classify_add_int normalize nodelta
    1247                                              >intsize_eq_elim_true >intsize_eq_elim_true
    1248                                              whd in match (opt_to_res ???); whd in match (opt_to_res ???);
    1249                                              whd in match (smaller_integer_val ?????); normalize nodelta
    1250                                              >sz_eq_identity >sz_eq_identity normalize nodelta
    1251                                              try @conj try @conj try //
    1252                                              >integer_add_cast_le //                                     
    1253                                          | 2: #_ (* subtraction case *)
    1254                                              >Hval_lhs >Hval_rhs destruct       
    1255                                              whd in match (sem_binary_operation Osub ?????);
    1256                                              whd in match (sem_binary_operation Osub ?????); normalize nodelta
    1257                                              >classify_sub_int >classify_sub_int normalize nodelta
    1258                                              >intsize_eq_elim_true >intsize_eq_elim_true
    1259                                              whd in match (opt_to_res ???); whd in match (opt_to_res ???);
    1260                                              whd in match (smaller_integer_val ?????); normalize nodelta
    1261                                              >sz_eq_identity >sz_eq_identity normalize nodelta
    1262                                              try @conj try @conj try //
    1263                                              >integer_sub_cast_le //
    1264                                          ]
    1265                                      ]
    1266                                  ]
    1267                              ]
    1268                          ]
    1269                      ]
    1270                  ]
    1271              ]
     1318                     cases (exec_expr ge en m lhs);
     1319                     try // * #val_lhs #trace_lhs normalize nodelta
     1320                     cases (exec_expr ge en m rhs);
     1321                     try // * #val_rhs #trace_rhs normalize nodelta
     1322                     whd in match (m_bind ?????);
     1323                     (* specialize to the actual simplifiable operations. *)
     1324                     cases op in Hop_simplifiable_eq;                     
     1325                     [ 1,2: | *: normalize in ⊢ (% → ?); #H destruct (H) ] #_                     
     1326                     [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m)
     1327                     | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ]
     1328                     cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m)
     1329                     [ 1,3: #_ #_ #_ normalize @I ]
     1330                     #src_result #Hinversion_src elim (Hinversion_src src_result (refl ? (Some ? src_result)))
     1331                     #src_result_sz * #i1 * #i2 * * #Hval_lhs_eq #Hval_rhs_eq #Hsrc_result_eq
     1332                     whd in match (opt_to_res ???); whd in match (m_bind ?????); normalize nodelta
     1333                     >Hval_lhs_eq >Hval_rhs_eq #Hsmaller_rhs #Hsmaller_lhs
     1334                     whd
     1335                     #result_int #Hsrc_result >Hsrc_result in Hsrc_result_eq; #Hsrc_result_eq             
     1336                     lapply (sym_eq ??? Hsrc_result_eq) -Hsrc_result_eq #Hsrc_result_eq                     
     1337                     cut (src_result_sz = src_sz) [ 1,3: destruct // ] #Hsz_eq
     1338                     lapply Hsmaller_lhs lapply Hsmaller_rhs
     1339                     cases (exec_expr ge en m lhs1) normalize nodelta
     1340                     [ 2,4: destruct #error normalize in ⊢ (% → ?); #H @(False_ind … (H i1 (refl ? (Vint src_sz i1)))) ]
     1341                     * #val_lhs1 #trace_lhs1
     1342                     cases (exec_expr ge en m rhs1)
     1343                     [ 2,4: destruct #error #_ normalize in ⊢ (% → ?); #H @(False_ind … (H i2 (refl ? (Vint src_sz i2)))) ]
     1344                     * #val_rhs1 #trace_rhs1
     1345                     whd in match (m_bind ?????); normalize nodelta
     1346                     [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
     1347                          lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
     1348                     | 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m)
     1349                          lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m) ]
     1350                     cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) val_rhs1 (Tint target_sz target_sg) m)
     1351                     [ 1,3: destruct #_ #Hneg_inversion elim (Hneg_inversion (refl ? (None ?)))
     1352                            (* Proceed by case analysis on Hneg_inversion to prove the absurdity of this branch *)
     1353                            *
     1354                            [ 1,4: whd in ⊢ (? → % → ?); normalize nodelta
     1355                                   #Habsurd #Hcounterexample elim (Hcounterexample i1 (refl ? (Vint src_sz i1)))
     1356                                   #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd
     1357                                   @(False_ind … (Habsurd I))
     1358                            | 2,5: whd in ⊢ (? → ? → % → ?); normalize nodelta
     1359                                   #Habsurd #_ #Hcounterexample elim (Hcounterexample i2 (refl ? (Vint src_sz i2)))
     1360                                   #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd
     1361                                   @(False_ind … (Habsurd I))
     1362                            | 3,6: #dsz1 * #dsz2 * #j1 * #j2 * * #Hval_lhs1 #Hval_rhs1 #Hsz_neq
     1363                                   whd in ⊢ (% → % → ?); normalize nodelta
     1364                                   #Hsmaller_lhs #Hsmaller_rhs
     1365                                   elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1)))
     1366                                   #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le
     1367                                   elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2)))
     1368                                   #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_
     1369                                   destruct elim Hsz_neq #Habsurd @(Habsurd (refl ? target_sz))
     1370                           ]
     1371                     | 2,4: destruct #result #Hinversion #_ #Hsmaller_lhs #Hsmaller_rhs normalize nodelta
     1372                            elim (Hinversion result (refl ? (Some ? result)))
     1373                            #result_sz * #lhs_int * #rhs_int * * #Hlhs1_eq #Hrhs1_eq #Hop_eq
     1374                            elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1)))
     1375                            #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le
     1376                            elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2)))
     1377                            #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_
     1378                            destruct
     1379                            [ 1: %{(addition_n (bitsize_of_intsize target_sz)
     1380                                     (cast_int_int src_sz src_sg target_sz i1)
     1381                                     (cast_int_int src_sz src_sg target_sz i2))}
     1382                                 try @conj try @conj try @conj //
     1383                                 >integer_add_cast_le try //
     1384                            | 2: %{(subtraction (bitsize_of_intsize target_sz)
     1385                                    (cast_int_int src_sz src_sg target_sz i1)
     1386                                    (cast_int_int src_sz src_sg target_sz i2))}
     1387                                 try @conj try @conj try @conj //
     1388                                 >integer_sub_cast_le try //
     1389                            ]
     1390                     ] ] ] ]
    12721391| 19,20,21,22: destruct %1 try @refl
    12731392   elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs
     
    13351454       [ 1: // | 2: <Htype_castee1 //
    13361455       | 3: whd in match (exec_expr ??? (Expr ??));
    1337             >Htype_castee 
     1456            >Htype_castee
    13381457            (* Simplify the goal by culling impossible cases, using Hsmaller_val *)
    13391458            cases (exec_expr ge en m castee) in Hsmaller_eval;
    13401459            [ 2: #error //
    1341             | 1: * #castee_val #castee_trace cases (exec_expr ge en m castee1)
    1342               [ 2: #error #Hcontr @(False_ind … Hcontr)
    1343               | 1: * #castee1_val #castee1_trace #Hsmaller
    1344                    elim (smaller_integer_val_spec … Hsmaller)
    1345                    #int1 * #int2 * * * * #Hint1 #Hint2 #Hcast #Htrace #Hle
    1346                    normalize nodelta destruct whd in match (exec_cast ????);
    1347                    normalize nodelta >intsize_eq_elim_true whd
    1348                    >sz_eq_identity >sz_eq_identity whd try @conj try @conj
    1349                    [ 3: elim (necessary_conditions_spec … (sym_eq … Hconditions))
    1350                         [ 1: elim target_sz elim cast_sz normalize #Hlt try @I @(False_ind … Hlt)
    1351                         | 2: * #Hcast_eq #_ >Hcast_eq elim target_sz // ]
    1352                    | 2: @refl
    1353                    | 1: @cast_composition //
    1354                         elim (necessary_conditions_spec … (sym_eq … Hconditions)) (* Clearly suboptimal stuff in this mess *)
    1355                         [ 1: elim target_sz elim cast_sz normalize #Hlt try @I @(False_ind … Hlt)
    1356                         | 2: * #Hcast_eq #_ >Hcast_eq elim target_sz // ]                       
    1357                    ]
    1358               ]
    1359             ]
    1360        ]
    1361   ]
     1460            | 1: * #castee_val #castee_trace #Hsmaller normalize nodelta
     1461              lapply (exec_cast_inv castee_val src_sz src_sg cast_sz cast_sg m)
     1462              cases (exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg))
     1463              [ 2: #error #_ @I
     1464              | 1: #result #Hinversion elim (Hinversion result (refl ? (OK ? result)))
     1465                   #castee_int * #Hcastee_val_eq #Hresult_eq
     1466                   whd in match (m_bind ?????);
     1467                   #result_int #Hresult_eq2
     1468                   cases (exec_expr ge en m castee1) in Hsmaller;
     1469                   [ 2: #error normalize in ⊢ (% → ?); #Habsurd
     1470                        @(False_ind … (Habsurd castee_int Hcastee_val_eq))
     1471                   | 1: * #val1 #trace1 whd in ⊢ (% → ?); normalize nodelta
     1472                        #Hsmaller elim (Hsmaller castee_int Hcastee_val_eq)
     1473                        #val1_int * * * #Hval1_eq #Hval1_int_eq #Hcastee_trace_eq
     1474                        destruct #Hle %{(cast_int_int src_sz src_sg target_sz castee_int)}
     1475                        try @conj try @conj try @conj try //                                               
     1476                        [ 1: @cast_composition ] try assumption
     1477                        elim (necessary_conditions_spec … (sym_eq … Hconditions))
     1478                        [ 2,4: * #Heq >Heq #_ elim target_sz //
     1479                        | 1,3: #Hlt @(size_lt_to_le ?? Hlt) ]
     1480 ] ] ] ] ]
    13621481| 25,27: destruct
    13631482      inversion (Hcast2 ge en m)
     
    13651484           #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hresult_contr <Hresult_contr in Hresult;
    13661485           #Hcontr destruct
    1367       | 2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself. 
     1486      | 2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself.
    13681487              We did not successfuly cast the subexpression to target_sz, though. *)
    13691488           #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq
     
    13751494               [ 2,4: (* erroneous evaluation of the original expression *)
    13761495                     #error #Hsmaller_eval @SimFail @(ex_intro … error) //
    1377                | 1,3: * #val #trace
    1378                     cases (exec_expr ge en m castee2)
    1379                     [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … Hsmaller_eval)
    1380                     | 1,3: * #val1 #trace1 #Hsmaller_eval elim (smaller_integer_val_spec … Hsmaller_eval)
    1381                          #int1 * #int2 * * * * #Hint1 #Hint2 #Hcast #Htrace #Hle
    1382                          @SimOk * #val2 #trace2 normalize nodelta >Htype_castee
    1383                          whd in match (exec_cast ????);
    1384                          cases val in Hint1; normalize nodelta
    1385                          [ 1,6: #Hint1 destruct | 3,4,5,8,9,10: #foo #Hint1 destruct
    1386                          | 2,7: destruct cases src_sz in int1; #int1 * #int2 #Hint1
    1387                               whd in match (intsize_eq_elim ???????);
    1388                               whd in match (m_bind ?????);
    1389                               [ 1,5,9,10,14,18: (* correct cases *) destruct #H @H
    1390                               | 2,3,4,6,7,8,11,12,13,15,16,17: #Habsurd destruct ]
    1391                          ]
    1392                     ]
    1393               ]
    1394          | 3,6:  @SimFail /2 by refl, ex_intro/
    1395          ]
    1396     ]
     1496               | 1,3: * #val #trace normalize nodelta >Htype_castee
     1497                      lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m)
     1498                      cases (exec_cast m val (Tint src_sz src_sg) (Tint cast_sz cast_sg))
     1499                      [ 2,4: #error #_ #_ @SimFail /2 by ex_intro/
     1500                      | 1,3: #result #Hinversion elim (Hinversion result (refl ??))
     1501                             #val_int * #Hval_eq #Hresult_eq
     1502                             cases (exec_expr ge en m castee2)
     1503                             [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … (Hsmaller_eval val_int Hval_eq))
     1504                             | 1,3: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq)
     1505                                    #val1_int * * * #Hval1_eq #Hcast_eq #Htrace_eq #Hle
     1506                                    destruct @SimOk normalize #a #H @H ]
     1507                ] ]
     1508           | 3,6: @SimFail /2 by refl, ex_intro/
     1509      ] ]
    13971510| 26,28: destruct
    13981511      inversion (Hcast2 ge en m)
     
    14681581                                           cases (exec_expr ge en m iftrue) in Hsmaller_true;
    14691582                                           [ 2: #error #_ @I
    1470                                            | 1: * #val_true_branch #trace_true_branch
     1583                                           | 1: * #val_true_branch #trace_true_branch #Hsmaller
     1584                                                #val_true_branch #Hval_true_branch lapply Hsmaller -Hsmaller                                               
    14711585                                                cases (exec_expr ge en m iftrue1)
    1472                                                 [ 2: #error normalize in ⊢ (% → ?); #H @(False_ind … H)
    1473                                                 | 1: * #val_true1_branch #trace_true1_branch #Hsmaller
    1474                                                      elim (smaller_integer_val_spec … Hsmaller)
    1475                                                      #true_val * #true1_val * * * * #Htrue_val #Htrue1_val #Hcast
    1476                                                      #Htrace_eq #Hsize_le normalize nodelta destruct
    1477                                                      whd in match (smaller_integer_val ?????);
    1478                                                      >sz_eq_identity normalize nodelta
    1479                                                      >sz_eq_identity normalize nodelta
    1480                                                      try @conj try @conj // ]
    1481                                            ]
    1482                                      | 2: (* false branch taken. Same proof as above, different arguments ... *)
     1586                                                [ 2: #error normalize in ⊢ (% → ?); #Hsmaller
     1587                                                     @(False_ind … (Hsmaller val_true_branch Hval_true_branch))
     1588                                                | 1: * #val_true1_branch #trace_true1_branch #Hsmaller normalize nodelta
     1589                                                     elim (Hsmaller val_true_branch Hval_true_branch)
     1590                                                     #val_true1_int * * * #val_true1_branch #Hval_cast_eq #Htrace_eq #Hle
     1591                                                     %{val_true1_int} try @conj try @conj try @conj //
     1592                                           ] ]
     1593                                     | 2: (* false branch taken. Same proof as above, different arguments ... *)
     1594                                           cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg)
     1595                                           [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq
     1596                                                destruct (Htype_eq) @conj @refl ] * #Hsz_eq #Hsg_eq destruct
    14831597                                           cases (exec_expr ge en m iffalse) in Hsmaller_false;
    14841598                                           [ 2: #error #_ @I
    1485                                            | 1: * #val_false_branch #trace_false_branch
     1599                                           | 1: destruct * #val_false_branch #trace_false_branch #Hsmaller
     1600                                                #val_false_branch #Hval_false_branch lapply Hsmaller -Hsmaller
    14861601                                                cases (exec_expr ge en m iffalse1)
    1487                                                 [ 2: #error normalize in ⊢ (% → ?); #H @(False_ind … H)
    1488                                                 | 1: * #val_false1_branch #trace_false1_branch #Hsmaller
    1489                                                      elim (smaller_integer_val_spec … Hsmaller)
    1490                                                      #false_val * #false1_val * * * * #Hfalse_val #Hfalse1_val #Hcast
    1491                                                      #Htrace_eq #Hsize_le normalize nodelta destruct
    1492                                                      whd in match (smaller_integer_val ?????);
    1493                                                      cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg)
    1494                                                      [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq
    1495                                                           destruct (Htype_eq) @conj @refl
    1496                                                      | 2: * #Hsize_eq #Hsg_eq destruct                                                     
    1497                                                           >sz_eq_identity normalize nodelta
    1498                                                           >sz_eq_identity normalize nodelta
    1499                                                           try @conj try @conj try @refl assumption
    1500                                                      ]
    1501                                                 ]
    1502                                            ]
    1503                                       ]
    1504                               ]
    1505                          ]
    1506                     ]
    1507                ]
    1508           ]
    1509      ]
     1602                                                [ 2: #error normalize in ⊢ (% → ?); #Hsmaller
     1603                                                     @(False_ind … (Hsmaller val_false_branch Hval_false_branch))
     1604                                                | 1: * #val_false1_branch #trace_false1_branch #Hsmaller normalize nodelta
     1605                                                     elim (Hsmaller val_false_branch Hval_false_branch)
     1606                                                     #val_false1_int * * * #val_false1_branch #Hval_cast_eq #Htrace_eq #Hle
     1607                                                     %{val_false1_int} try @conj try @conj try @conj //
     1608                                           ] ]
     1609      ] ] ] ] ] ] ]
    15101610| 38,39,40: destruct
    15111611   elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq
     
    16011701           @(Inv_coerce_ok ??????? target_sz target_sg)
    16021702           [ 1,2: //
    1603            | 3: cases target_sz cases target_sg normalize try @conj try @conj try @refl try @I ]
     1703           | 3: @smaller_integer_val_identity ]
    16041704      | 2: #Hneq >(type_neq_not_identity … Hneq)
    16051705           %1 // @SimOk #a #H @H
     
    16511751              cases (exec_expr ge en m e1) in Hsmaller;
    16521752              [ 2: #error normalize //
    1653               | 1: * #val1 #trace1 cases (exec_expr ge en m e2)
    1654                    [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … Habsurd)
    1655                    | 1: * #val2 #trace #Hsmaller
    1656                         elim (smaller_integer_val_spec … Hsmaller)
    1657                         #i1 * #i2 * * * * #Hval1 #Hval2 #Hcast #Htrace_eq #Hsize_le
    1658                         normalize nodelta destruct whd in match (smaller_integer_val ?????);
    1659                         >sz_eq_identity >sz_eq_identity normalize nodelta
    1660                         try @conj try @conj try @conj try @refl assumption
     1753              | 1: * #val1 #trace1 #Hsmaller #val1_int #Hval1_eq                   
     1754                   cases (exec_expr ge en m e2) in Hsmaller;
     1755                   [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … (Habsurd val1_int Hval1_eq))
     1756                   | 1: * #val2 #trace #Hsmaller elim (Hsmaller val1_int Hval1_eq)
     1757                        #val2_int * * * #Hval2_eq #Hcast #Htrace #Hle normalize nodelta
     1758                        %{val2_int} try @conj try @conj try @conj //
    16611759                   ]
    16621760               ]
     
    17801878            cases (exec_expr ge en m castee) in Hsmaller;
    17811879            [ 2: #error #_ @SimFail /2 by ex_intro/
    1782             | 1: * #val #trace cases (exec_expr ge en m castee1)
    1783                  [ 2: #error #Habsurd @(False_ind … Habsurd)
    1784                  | 1: * #val1 #trace1 #Hsmaller elim (smaller_integer_val_spec … Hsmaller)
    1785                       #v1 * #v2 * * * * #Hval1 #Hval2 #Hcast #Htrace #Hle
    1786                       >Hsrc_type_eq normalize nodelta cases val in Hval1;
    1787                       [ 1: #Hval1 | 2: #sz #i #Hval1 | 3,4,5: #irrelevant #Hval1 ]
    1788                       [ 1,3,4,5: normalize @SimFail /2 by ex_intro/ ]
    1789                       whd in match (exec_cast ????);
    1790                       cases (sz_eq_dec sz src_sz)
    1791                       [ 2: #Hneq normalize nodelta
    1792                            >(intsize_eq_elim_false (res ?) sz src_sz ???? Hneq)
    1793                            @SimFail /2 by ex_intro/
    1794                       | 1: #Heq <Heq normalize nodelta >intsize_eq_elim_true
    1795                            destruct normalize
    1796                            @SimOk #a #H @H
     1880            | 1: * #val #trace normalize nodelta >Hsrc_type_eq
     1881                 lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m)
     1882                 cases (exec_cast m val ??)
     1883                 [ 2: #error #_ #_ @SimFail /2 by ex_intro/
     1884                 | 1: #result #Hinversion elim (Hinversion result (refl ??))
     1885                      #val_int * #Hval_eq #Hcast
     1886                      cases (exec_expr ge en m castee1)
     1887                      [ 2: #error #Habsurd normalize in Habsurd; @(False_ind … (Habsurd val_int Hval_eq))
     1888                      | 1: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq)
     1889                           #val1_int * * * #Hval1_int #Hval18int #Htrace #Hle
     1890                           @SimOk destruct normalize // ]
    17971891                      ]
    1798                  ]
    1799             ]
     1892             ]
    18001893      | 2: @SimFail /2 by ex_intro/
    18011894      | 3: >Htarget_type_eq //
     
    20462139// qed.
    20472140
    2048 include "Clight/CexecInd.ma".
     2141
     2142definition expr_lvalue_ind_combined ≝
     2143λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
     2144conj ??
     2145 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
     2146 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
    20492147 
    20502148lemma simulation_transitive : ∀A,r0,r1,r2. simulate A r0 r1 → simulate A r1 r2 → simulate A r0 r2.
     
    30123110     whd in match (exec_step ??) in ⊢ (% → %);
    30133111     #Habsurd destruct (Habsurd)
    3014 ] qed.
    3015 
     3112]
Note: See TracChangeset for help on using the changeset viewer.