Ignore:
Timestamp:
Jan 23, 2013, 2:38:06 PM (7 years ago)
Author:
garnier
Message:

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2468 r2588  
    608608λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ].
    609609
    610 (* Inversion principle for integer addition *)
    611 lemma iadd_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
     610(* Inversion principle for integer addition - wrapper around lemma in frontend_misc *)
     611lemma iadd_inv : ∀sz,sg,v1,v2,m,target_ty,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = Some ? r →
    612612                                    ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (addition_n (bitsize_of_intsize dsz) i1 i2)).
    613 #sz #sg #v1 #v2 #m #r
    614 elim v1
    615 [ 1: | 2: #sz' #i | 3: | 4: #ptr ]
    616 whd in ⊢ ((??%?) → ?); normalize nodelta
    617 >classify_add_int normalize nodelta #H destruct
    618 elim v2 in H;
    619 [ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ]
    620 whd in ⊢ ((??%?) → ?); #H destruct
    621 elim (sz_eq_dec sz' sz'')
    622 [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
    623 | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
    624 ] qed.
     613#sz #sg #v1 #v2 #m #ty #r whd @sem_add_ii_inversion qed.
    625614
    626615(* Inversion principle for integer subtraction. *)
    627 lemma isub_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
    628                                     ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)).
    629 #sz #sg #v1 #v2 #m #r
    630 elim v1
    631 [ 1: | 2: #sz' #i | 3: | 4: #ptr ]
    632 whd in ⊢ ((??%?) → ?); normalize nodelta
    633 >classify_sub_int normalize nodelta #H destruct
    634 elim v2 in H;
    635 [ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ]
    636 whd in ⊢ ((??%?) → ?); #H destruct
    637 elim (sz_eq_dec sz' sz'')
    638 [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
    639 | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
    640 ] qed.
     616lemma isub_inv : ∀sz,sg,v1,v2,m,target_ty,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = Some ? r →
     617                                      ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)).
     618#sz #sg #v1 #v2 #m #ty #r whd @sem_sub_ii_inversion qed.
    641619
    642620definition is_int : val → Prop ≝
     
    647625
    648626(* "negative" (in the sense of ¬ Some) inversion principle for integer addition *)
    649 lemma neg_iadd_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
     627lemma neg_iadd_inv : ∀sz,sg,v1,v2,m,target_ty. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = None ? →
    650628                                        ¬ (is_int v1) ∨ ¬ (is_int v2) ∨
    651629                                        ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
    652 #sz #sg #v1 #v2 #m
     630#sz #sg #v1 #v2 #m #ty
    653631elim v1
    654632[ 1: | 2: #sz' #i | 3: | 4: #ptr ]
     
    666644
    667645(* "negative" inversion principle for integer subtraction *)
    668 lemma neg_isub_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
     646lemma neg_isub_inv : ∀sz,sg,v1,v2,m,target_ty. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = None ? →
    669647                                        ¬ (is_int v1) ∨ ¬ (is_int v2) ∨
    670648                                        ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
    671 #sz #sg #v1 #v2 #m
     649#sz #sg #v1 #v2 #m #target_ty
    672650elim v1
    673651[ 1: | 2: #sz' #i | 3: | 4: #ptr ]
     
    684662] qed.
    685663
    686 lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m.
    687    ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?.
    688 #op #sz #sg #v1 #v2 #m #H
     664lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m,target_ty.
     665   ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = None ?.
     666#op #sz #sg #v1 #v2 #m #target_ty #H
    689667elim op normalize in match (binop_simplifiable ?); #H destruct
    690668elim v1 in H;
    691669[ 1,5: | 2,6: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,7: | 4,8: #ptr ]
    692670#_
    693 whd in match (sem_binary_operation ??????); normalize nodelta
     671whd in match (sem_binary_operation ???????); normalize nodelta
    694672>classify_add_int normalize nodelta //
    695673>classify_sub_int normalize nodelta //
     
    11141092                     cases op in Hop_simplifiable_eq;                 
    11151093                     [ 1,2: | *: normalize in ⊢ (% → ?); #H destruct (H) ] #_
    1116                      [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m)
    1117                      | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ]
    1118                      cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m)
     1094                     [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m (Tint src_sz src_sg))
     1095                     | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m (Tint src_sz src_sg)) ]
     1096                     cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m (Tint src_sz src_sg))
    11191097                     [ 1,3: #_ #_ #_ normalize @I ]
    11201098                     #src_result #Hinversion_src elim (Hinversion_src src_result (refl ? (Some ? src_result)))
     
    11341112                     * #val_rhs1 #trace_rhs1
    11351113                     whd in match (m_bind ?????); normalize nodelta
    1136                      [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
    1137                           lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
    1138                      | 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m)
    1139                           lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m) ]
    1140                      cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) val_rhs1 (Tint target_sz target_sg) m)
     1114                     [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg))
     1115                          lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg))
     1116                     | 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg))
     1117                          lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg)) ]
     1118                     cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg)
     1119                                                   val_rhs1 (Tint target_sz target_sg) m (Tint target_sz target_sg))
    11411120                     [ 1,3: destruct #_ #Hneg_inversion elim (Hneg_inversion (refl ? (None ?)))
    11421121                            (* Proceed by case analysis on Hneg_inversion to prove the absurdity of this branch *)
     
    12701249                        [ 2,4: * #Heq >Heq #_ elim target_sz //
    12711250                        | 1,3: #Hlt @(size_lt_to_le ?? Hlt) ]
    1272  ] ] ] ] ] 
     1251 ] ] ] ] ]
    12731252| 23,25: destruct
    12741253      inversion (Hcast2 ge en m)
     
    14611440                     normalize nodelta >Htype_eq_lhs
    14621441                     cases (exec_bool_of_val lhs_val (typeof lhs1))
    1463                        [ 2,4: #error normalize @SimFailNicely
     1442                     [ 2,4: #error normalize @SimFailNicely
    14641443                     | 1,3: *
    14651444                         whd in match (m_bind ?????);
Note: See TracChangeset for help on using the changeset viewer.