Changeset 2572


Ignore:
Timestamp:
Jan 9, 2013, 1:23:29 PM (7 years ago)
Author:
garnier
Message:

Progress on toCminorCorrectness.

Location:
src/Clight
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2565 r2572  
    326326(* Useful facts on blocks. *)
    327327(* --------------------------------------------------------------------------- *)
     328
     329lemma eq_block_to_refl : ∀b1,b2. eq_block b1 b2 = true → b1 = b2.
     330#b1 #b2 @(eq_block_elim … b1 b2)
     331[ //
     332| #_ #Habsurd destruct ] qed.
    328333
    329334lemma not_eq_block : ∀b1,b2. b1 ≠ b2 → eq_block b1 b2 = false.
  • src/Clight/memoryInjections.ma

    r2569 r2572  
    388388| 3: #Habsurd destruct (Habsurd)
    389389| 4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ]
    390 qed.
     390qed.
     391
     392lemma value_eq_null_inversion :
     393  ∀E,v. value_eq E Vnull v → v = Vnull.
     394#E #v #Heq inversion Heq //
     395#p1 #p2 #Htranslate #Habsurd lapply (jmeq_to_eq ??? Habsurd)
     396#Habsurd' destruct
     397qed.
    391398
    392399(* A cleaner version of inversion for [value_eq] *)
     
    443450    Zltb (block_id b) (nextblock m) = true ∧
    444451    Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧
    445  
    446452    Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true.
    447453#ty #m * #brg #bid #off #v
  • src/Clight/toCminor.ma

    r2568 r2572  
    405405[ aop_case_ii sz sg ⇒
    406406    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
    407     [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2)
    408     | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2)
     407    [ Unsigned ⇒ λe1,e2.  typ_should_eq ??? (Op2 ??? (Oshru …) e1 e2)
     408    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oshr …) e1 e2)
    409409    ]
    410410(* no float case *)
     
    417417[ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I8 Unsigned sz sg) e)
    418418| _ ⇒ Error ? (msg TypeMismatch)
    419 ].
    420 
     419]. 
     420 
    421421definition translate_cmp ≝
    422422λc,ty1,ty2,ty'.
     
    457457| Oxor ⇒ translate_misc_aop ty1 ty2 ty Oxor e1 e2
    458458| Oshl ⇒ translate_misc_aop ty1 ty2 ty Oshl e1 e2
    459 | Oshr ⇒ translate_shr ty1 ty2 ty e1 e2
     459(*| Oshr ⇒ translate_misc_aop ty1 ty2 ty Oshr e1 e2 *)
     460| Oshr ⇒ translate_shr ty1 ty2 ty e1 e2  (* split on signed/unsigned *)
    460461| Oeq ⇒ translate_cmp Ceq ty1 ty2 ty e1 e2
    461462| One ⇒ translate_cmp Cne ty1 ty2 ty e1 e2
  • src/Clight/toCminorCorrectness.ma

    r2569 r2572  
    359359qed.
    360360
    361 include "Clight/CexecSound.ma".
    362 
    363361lemma lookup_exec_alloc :
    364362  ∀source_variables, initial_env, env, var_id, clb, m, m'.
     
    593591qed.
    594592
     593(*
     594lemma classify_cmp_inversion :
     595  ∀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*)   
     602
    595603lemma classify_aop_inversion :
    596604  ∀ty1,ty2.
     
    762770qed.
    763771
     772lemma sem_mod_inversion_s :
     773  ∀sz.
     774  ∀v1,v2,res.
     775  sem_mod v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
     776  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     777              match modulus_s ? i1 i2 with
     778              [ Some q ⇒  res =  (Vint sz' q)
     779              | None ⇒ False ].
     780#sz *
     781[ | #sz' #i' | | #p' ]
     782#v2 #res
     783whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     784>type_eq_dec_true normalize nodelta
     785#H destruct
     786cases v2 in H; normalize nodelta
     787[ | #sz2' #i2' | | #p2' ]
     788#Heq destruct
     789%{sz'}
     790lapply Heq -Heq
     791cases sz' in i'; #i' 
     792whd in match (intsize_eq_elim ???????);
     793cases sz2' in i2'; #i2' normalize nodelta
     794whd in match (option_map ????); #Hdiv destruct
     795%{i'} %{i2'} @conj try @conj try @conj try @refl
     796cases (modulus_s ???) in Hdiv;
     797[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     798qed.
     799
     800lemma sem_mod_inversion_u :
     801  ∀sz.
     802  ∀v1,v2,res.
     803  sem_mod v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
     804  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     805              match modulus_u ? i1 i2 with
     806              [ Some q ⇒  res =  (Vint sz' q)
     807              | None ⇒ False ].
     808#sz *
     809[ | #sz' #i' | | #p' ]
     810#v2 #res
     811whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     812>type_eq_dec_true normalize nodelta
     813#H destruct
     814cases v2 in H; normalize nodelta
     815[ | #sz2' #i2' | | #p2' ]
     816#Heq destruct
     817%{sz'}
     818lapply Heq -Heq
     819cases sz' in i'; #i' 
     820whd in match (intsize_eq_elim ???????);
     821cases sz2' in i2'; #i2' normalize nodelta
     822whd in match (option_map ????); #Hdiv destruct
     823%{i'} %{i2'} @conj try @conj try @conj try @refl
     824cases (modulus_u ???) in Hdiv;
     825[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     826qed.
     827
     828lemma sem_and_inversion :
     829  ∀v1,v2,res.
     830  sem_and v1 v2 = Some ? res →
     831  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     832              res = Vint sz' (conjunction_bv ? i1 i2).
     833*
     834[ | #sz' #i' | | #p' ]
     835#v2 #res
     836whd in ⊢ ((??%?) → ?);
     837#H destruct
     838cases v2 in H; normalize nodelta
     839[ | #sz2' #i2' | | #p2' ]
     840#Heq destruct
     841%{sz'}
     842lapply Heq -Heq
     843cases sz' in i'; #i' 
     844whd in match (intsize_eq_elim ???????);
     845cases sz2' in i2'; #i2' normalize nodelta
     846#H destruct
     847%{i'} %{i2'} @conj try @conj try @conj try @refl
     848qed.
     849
     850lemma sem_or_inversion :
     851  ∀v1,v2,res.
     852  sem_or v1 v2 = Some ? res →
     853  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     854              res = Vint sz' (inclusive_disjunction_bv ? i1 i2).
     855*
     856[ | #sz' #i' | | #p' ]
     857#v2 #res
     858whd in ⊢ ((??%?) → ?);
     859#H destruct
     860cases v2 in H; normalize nodelta
     861[ | #sz2' #i2' | | #p2' ]
     862#Heq destruct
     863%{sz'}
     864lapply Heq -Heq
     865cases sz' in i'; #i' 
     866whd in match (intsize_eq_elim ???????);
     867cases sz2' in i2'; #i2' normalize nodelta
     868#H destruct
     869%{i'} %{i2'} @conj try @conj try @conj try @refl
     870qed.
     871
     872lemma sem_xor_inversion :
     873  ∀v1,v2,res.
     874  sem_xor v1 v2 = Some ? res →
     875  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     876              res = Vint sz' (exclusive_disjunction_bv ? i1 i2).
     877*
     878[ | #sz' #i' | | #p' ]
     879#v2 #res
     880whd in ⊢ ((??%?) → ?);
     881#H destruct
     882cases v2 in H; normalize nodelta
     883[ | #sz2' #i2' | | #p2' ]
     884#Heq destruct
     885%{sz'}
     886lapply Heq -Heq
     887cases sz' in i'; #i' 
     888whd in match (intsize_eq_elim ???????);
     889cases sz2' in i2'; #i2' normalize nodelta
     890#H destruct
     891%{i'} %{i2'} @conj try @conj try @conj try @refl
     892qed.
     893
     894lemma sem_shl_inversion :
     895  ∀v1,v2,res.
     896  sem_shl v1 v2 = Some ? res →
     897  ∃sz1,sz2,i1,i2.
     898              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
     899              res = Vint sz1 (shift_left bool (bitsize_of_intsize sz1)
     900                                  (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false) ∧
     901              lt_u (bitsize_of_intsize sz2) i2
     902                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true.
     903*
     904[ | #sz' #i' | | #p' ]
     905#v2 #res
     906whd in ⊢ ((??%?) → ?);
     907#H destruct
     908cases v2 in H; normalize nodelta
     909[ | #sz2' #i2' | | #p2' ]
     910#Heq destruct
     911%{sz'} %{sz2'}
     912lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
     913%{i'} %{i2'}
     914>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
     915qed.
     916
     917lemma sem_shr_inversion :
     918  ∀v1,v2,sz,sg,res.
     919  sem_shr v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
     920  ∃sz1,sz2,i1,i2.
     921              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
     922              lt_u (bitsize_of_intsize sz2) i2
     923                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true ∧
     924              match sg with
     925              [ Signed ⇒
     926                 res =
     927                   (Vint sz1
     928                    (shift_right bool (7+pred_size_intsize sz1*8)
     929                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1
     930                     (head' bool (7+pred_size_intsize sz1*8) i1)))               
     931              | Unsigned ⇒
     932                 res =
     933                   (Vint sz1
     934                    (shift_right bool (7+pred_size_intsize sz1*8)
     935                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false))
     936              ].
     937*
     938[ | #sz' #i' | | #p' ]
     939#v2 #sz * #res
     940whd in ⊢ ((??%?) → ?);
     941whd in match (classify_aop ??);
     942>type_eq_dec_true normalize nodelta
     943#H destruct
     944cases v2 in H; normalize nodelta
     945[ | #sz2' #i2' | | #p2'
     946| | #sz2' #i2' | | #p2' ]
     947#Heq destruct
     948%{sz'} %{sz2'}
     949lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
     950%{i'} %{i2'}
     951>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
     952qed.
     953
     954lemma complete_cmp_inversion :
     955  ∀ty:type.
     956  ∀e:expr (ASTint I8 Unsigned).
     957  ∀r:expr (typ_of_type ty).
     958   complete_cmp ty e = return r →
     959   ∃sz,sg. ty = Tint sz sg ∧
     960           r ≃ Op1 (ASTint I8 Unsigned) (ASTint sz sg) (Ocastint I8 Unsigned sz sg) e.
     961*
     962[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     963| #structname #fieldspec | #unionname #fieldspec | #id ]
     964#e whd in match (typ_of_type ?);
     965#r whd in ⊢ ((??%%) → ?);
     966#H destruct
     967%{sz} %{sg} @conj try @refl @refl_jmeq
     968qed.
     969
     970
     971lemma sem_cmp_int_inversion :
     972  ∀v1,v2,sz,sg,op,m,res.
     973   sem_cmp op v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? res →
     974   ∃sz,i1,i2. v1 = Vint sz i1 ∧
     975              v2 = Vint sz i2 ∧
     976    match sg with
     977    [ Unsigned ⇒ of_bool (cmpu_int ? op i1 i2) = res
     978    | Signed   ⇒ of_bool (cmp_int ? op i1 i2) = res
     979    ].
     980#v1 #v2 #sz0 #sg #op * #contents #next #Hnext #res
     981whd in ⊢ ((??%?) → ?);
     982whd in match (classify_cmp ??); >type_eq_dec_true normalize nodelta
     983cases v1
     984[ | #sz #i | | #p ] normalize nodelta
     985#H destruct
     986cases v2 in H;
     987[ | #sz' #i' | | #p' ] normalize nodelta
     988#H destruct lapply H -H
     989cases sz in i; #i
     990cases sz' in i'; #i' cases sg normalize nodelta
     991whd in match (intsize_eq_elim ???????); #H destruct
     992[ 1,2: %{I8}
     993| 3,4: %{I16}
     994| 5,6: %{I32} ] 
     995%{i} %{i'} @conj try @conj try @refl
     996qed.
     997
     998lemma typ_of_ptr_type : ∀ty',n. typ_of_type (ptr_type ty' n) = ASTptr.
     999#ty' * // qed.
     1000
     1001lemma sem_cmp_ptr_inversion :
     1002  ∀v1,v2,ty',n,op,m,res.
     1003   sem_cmp op v1 (ptr_type ty' n) v2 (ptr_type ty' n) m = Some ? res →
     1004   (∃p1,p2. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧
     1005                 valid_pointer m p1 = true ∧
     1006                 valid_pointer m p2 = true ∧
     1007                 (if eq_block (pblock p1) (pblock p2)
     1008                  then Some ? (of_bool (cmp_offset op (poff p1) (poff p2)))
     1009                  else sem_cmp_mismatch op) = Some ? res) ∨
     1010   (∃p1. v1 = Vptr p1 ∧ v2 = Vnull ∧ sem_cmp_mismatch op = Some ? res) ∨                 
     1011   (∃p2. v1 = Vnull ∧ v2 = Vptr p2 ∧ sem_cmp_mismatch op = Some ? res) ∨
     1012   (v1 = Vnull ∧ v2 = Vnull ∧ sem_cmp_match op = Some ? res).
     1013* [ | #sz #i | | #p ] normalize nodelta
     1014#v2 #ty' #n #op
     1015* #contents #nextblock #Hnextblock #res whd in ⊢ ((??%?) → ?);
     1016whd in match (classify_cmp ??); cases n normalize nodelta
     1017[ 2,4,6,8: #array_len ]
     1018whd in match (ptr_type ty' ?);
     1019whd in match (if_type_eq ?????);
     1020>type_eq_dec_true normalize nodelta
     1021#H destruct
     1022cases v2 in H; normalize nodelta
     1023[ | #sz' #i' | | #p'
     1024| | #sz' #i' | | #p'
     1025| | #sz' #i' | | #p'
     1026| | #sz' #i' | | #p' ]
     1027#H destruct
     1028try /6 by or_introl, or_intror, ex_intro, conj/
     1029[ 1: %1 %1 %2 %{p} @conj try @conj //
     1030| 3: %1 %1 %2 %{p} @conj try @conj //
     1031| *: %1 %1 %1 %{p} %{p'}
     1032     cases (valid_pointer (mk_mem ???) p) in H; normalize nodelta
     1033     cases (valid_pointer (mk_mem contents nextblock Hnextblock) p') normalize nodelta #H
     1034     try @conj try @conj try @conj try @conj try @conj try @refl try @H
     1035     destruct
     1036] qed.
     1037
     1038lemma pointer_translation_eq_block :
     1039  ∀E,p1,p2,p1',p2'.
     1040  pointer_translation p1 E = Some ? p1' →
     1041  pointer_translation p2 E = Some ? p2' →
     1042  eq_block (pblock p1) (pblock p2) = true →
     1043  eq_block (pblock p1') (pblock p2') = true.
     1044#E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2'
     1045#H1 #H2 #Heq_block
     1046lapply (eq_block_to_refl … Heq_block) #H destruct (H)
     1047lapply H1 lapply H2 -H1 -H2
     1048whd in ⊢ ((??%?) → (??%?) → ?);
     1049cases (E b2) normalize nodelta
     1050[ #Habsurd destruct ]
     1051* #bx #ox normalize nodelta #Heq1 #Heq2 destruct
     1052@eq_block_b_b
     1053qed.
     1054
     1055lemma pointer_translation_cmp_offset :
     1056  ∀E,p1,p2,p1',p2',op.
     1057  pblock p1 = pblock p2 →
     1058  pointer_translation p1 E = Some ? p1' →
     1059  pointer_translation p2 E = Some ? p2' →
     1060  cmp_offset op (poff p1) (poff p2) = cmp_offset op (poff p1') (poff p2').
     1061#E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2' #op #Heq destruct
     1062whd in ⊢ ((??%?) → (??%?) → ?);
     1063cases (E b2) normalize nodelta
     1064[ #H destruct ]
     1065* #bx #ox normalize nodelta
     1066#Heq1 #Heq2 destruct cases op
     1067[ @sym_eq @eq_offset_translation
     1068| @sym_eq @neq_offset_translation
     1069| @cthulhu (* !!!! TODO !!!! *)
     1070| @cthulhu (* !!!! TODO !!!! *)
     1071| @cthulhu (* !!!! TODO !!!! *)
     1072| @cthulhu (* !!!! TODO !!!! *)
     1073] qed.
     1074
     1075(* The two following lemmas are just noise. *)
     1076
    7641077lemma expr_vars_fix_ptr_type :
    7651078  ∀ty',optlen.
     
    7801093qed.
    7811094
    782 (* This lemma is just noise. *)
    7831095lemma eval_expr_rewrite_aux :
    7841096  ∀genv.
     
    8111123      a sign extension on i in expressions (ptr + i) whereas Cminor case splits on
    8121124      the sign of i, producing either a sign extension or a zero extension.
     1125   3) something similar to 1) happens for binary comparison operators. Clight generates
     1126      systematically a 32 bit value for the outcome of the comparison and lives with it,
     1127      but toCminor actually generates something 8 bit and casts it back to the context type.
     1128   4) we need some proof that we don't blow the stack during the transformation. Otherwise,
     1129      a problem appears when we prove semantics preservation for pointer < comparison
     1130      (we might wrap up the rhs and end SNAFU).
    8131131 *)
    8141132lemma eval_expr_sim :
     
    10561374       >intsize_eq_elim_true #Heq destruct (Heq)
    10571375       %2
    1058      | 4: (* div *)
     1376     | 4,5: (* div *)
    10591377       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
    10601378       [ 2,4: #Hclassify >Hclassify normalize nodelta
     
    10721390       whd in match (typ_of_type (Tint ??));
    10731391       #lhs #rhs #Htyp_should_eq
    1074        [ cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
    1075        | cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
     1392       [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
     1393       | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
    10761394       -Htyp_should_eq
    10771395       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
     
    11021420       whd in match (eval_binop ???????);
    11031421       whd in Hsem_binary:(??%?);
    1104        lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    1105        * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1106        [ cases (sem_div_inversion_s … Hsem_binary)
    1107        | cases (sem_div_inversion_u … Hsem_binary) ]
     1422       [ 1,3: (* div*)
     1423          lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     1424          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
     1425          [ cases (sem_div_inversion_s … Hsem_binary)
     1426          | cases (sem_div_inversion_u … Hsem_binary) ]
     1427       | 2,4: (* mod *)
     1428          lapply (mod_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     1429          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
     1430          [ cases (sem_mod_inversion_s … Hsem_binary)
     1431          | cases (sem_mod_inversion_u … Hsem_binary) ]
     1432       ]
    11081433       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
    11091434       #Hcm_lhs #Hcm_rhs #Hcm_val
     
    11121437       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
    11131438       >intsize_eq_elim_true normalize nodelta
    1114        [ cases (division_s ???) in Hcm_val; normalize nodelta
    1115          [ @False_ind
    1116          | #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2 ]
    1117        | cases (division_u ???) in Hcm_val; normalize nodelta
    1118          [ @False_ind
    1119          | #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2 ] ]
    1120      | 5: (* mod *) @cthulhu
    1121      | 6: (* and *) @cthulhu
    1122      | 7: (* or *)  @cthulhu
    1123      | 8: (* xor *) @cthulhu
    1124      | 9: (* shl *) @cthulhu
    1125      | 10: (* shr *) @cthulhu
    1126      | 11: (* eq *) @cthulhu
    1127      | 12: (* ne *) @cthulhu
    1128      | 13: (* lt *) @cthulhu
    1129      | 14: (* gt *) @cthulhu
    1130      | 15: (* le *) @cthulhu
    1131      | 16: (* ge *) @cthulhu ]
     1439       [ cases (division_s ???) in Hcm_val;
     1440       | cases (division_u ???) in Hcm_val;
     1441       | cases (modulus_s ???) in Hcm_val;
     1442       | cases (modulus_u ???) in Hcm_val; ]
     1443       normalize nodelta
     1444       [ 1,3,5,7: @False_ind ]
     1445       #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2
     1446     | 6,7,8: (* and,or,xor *)
     1447       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
     1448       [ 2,4,6: #Hclassify >Hclassify normalize nodelta
     1449            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
     1450       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
     1451       whd in match (typeof ?); #e'
     1452       * #sz * #sg * *
     1453       whd in match (typeof ?) in ⊢ (% → % → ?);
     1454       #Htypeof_e1 #Htypeof_e2
     1455       >Htypeof_e1 >Htypeof_e2
     1456       whd in match (typeof ?) in ⊢ (% → % → % → ?);
     1457       #Hclassify
     1458       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
     1459       normalize nodelta
     1460       whd in match (typ_of_type (Tint ??));
     1461       #lhs #rhs #Htyp_should_eq
     1462       cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
     1463       -Htyp_should_eq
     1464       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
     1465       <Heq_e' -Heq_e'
     1466       #Hexec
     1467       #Hexpr_vars_rhs #Hexpr_vars_lhs
     1468       #Htranslate_rhs #Htranslate_lhs
     1469       * #Hyp_present_lhs #Hyp_present_rhs
     1470       #Hind_rhs #Hind_lhs
     1471       cases (bind_inversion ????? Hexec) -Hexec
     1472       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
     1473       cases (bind_inversion ????? Hexec) -Hexec
     1474       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
     1475       cases (bind_inversion ????? Hexec) -Hexec
     1476       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1477       lapply (opt_to_res_inversion ???? Hsem) -Hsem
     1478       whd in match (typeof ?); whd in match (typeof ?);
     1479       #Hsem_binary
     1480       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
     1481       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
     1482       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
     1483       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
     1484       whd in match (eval_expr ???????);
     1485       whd in match (proj1 ???);
     1486       >Heval_lhs normalize nodelta
     1487       >Heval_rhs normalize nodelta
     1488       whd in match (m_bind ?????);
     1489       whd in match (eval_binop ???????);
     1490       whd in Hsem_binary:(??%?);
     1491       [ 1: (* and *)
     1492          lapply (and_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     1493           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
     1494          cases (sem_and_inversion … Hsem_binary)
     1495       | 2: (* or *)
     1496          lapply (or_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     1497           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
     1498          cases (sem_or_inversion … Hsem_binary)
     1499       | 3: (* xor *)
     1500          lapply (xor_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     1501           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
     1502          cases (sem_xor_inversion … Hsem_binary)
     1503       ]
     1504       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
     1505       #Hcm_lhs #Hcm_rhs #Hcm_val
     1506       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
     1507       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
     1508       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
     1509       >intsize_eq_elim_true normalize nodelta
     1510       [ 1: %{(Vint cm_vsz (conjunction_bv … cm_lhs_v cm_rhs_v))}
     1511       | 2: %{(Vint cm_vsz (inclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
     1512       | 3: %{(Vint cm_vsz (exclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
     1513       ]
     1514       @conj try @refl >Hcm_val %2
     1515     | 9,10: (* shl, shr *)
     1516       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
     1517       [ 2,4: #Hclassify >Hclassify normalize nodelta
     1518            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
     1519       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
     1520       whd in match (typeof ?); #e'
     1521       * #sz * * * *
     1522       whd in match (typeof ?) in ⊢ (% → % → ?);
     1523       #Htypeof_e1 #Htypeof_e2
     1524       >Htypeof_e1 >Htypeof_e2
     1525       whd in match (typeof ?) in ⊢ (% → % → % → ?);
     1526       #Hclassify
     1527       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
     1528       normalize nodelta
     1529       whd in match (typ_of_type (Tint ??));
     1530       #lhs #rhs #Htyp_should_eq
     1531       [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
     1532       | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
     1533       -Htyp_should_eq
     1534       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
     1535       <Heq_e' -Heq_e'
     1536       #Hexec
     1537       #Hexpr_vars_rhs #Hexpr_vars_lhs
     1538       #Htranslate_rhs #Htranslate_lhs
     1539       * #Hyp_present_lhs #Hyp_present_rhs
     1540       #Hind_rhs #Hind_lhs
     1541       cases (bind_inversion ????? Hexec) -Hexec
     1542       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
     1543       cases (bind_inversion ????? Hexec) -Hexec
     1544       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
     1545       cases (bind_inversion ????? Hexec) -Hexec
     1546       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1547       lapply (opt_to_res_inversion ???? Hsem) -Hsem
     1548       whd in match (typeof ?); whd in match (typeof ?);
     1549       #Hsem_binary
     1550       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
     1551       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
     1552       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
     1553       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
     1554       whd in match (eval_expr ???????);
     1555       whd in match (proj1 ???);
     1556       >Heval_lhs normalize nodelta
     1557       >Heval_rhs normalize nodelta
     1558       whd in match (m_bind ?????);
     1559       whd in match (eval_binop ???????);
     1560       whd in Hsem_binary:(??%?);
     1561       [ 1,3: (* shl *)
     1562          lapply (shl_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     1563          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
     1564          cases (sem_shl_inversion … Hsem_binary)
     1565          #sz1 * #sz2 * #lhs_i * #rhs_i * * *
     1566          #Hcl_lhs #Hcl_rhs #Hcl_val #Hshift_ok
     1567          destruct (Hcl_lhs Hcl_rhs)
     1568          >(value_eq_int_inversion … Hvalue_eq_lhs)
     1569          >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
     1570          >Hshift_ok normalize nodelta
     1571          %{(Vint sz1
     1572               (shift_left bool (bitsize_of_intsize sz1)
     1573               (nat_of_bitvector (bitsize_of_intsize sz2) rhs_i) lhs_i false))}
     1574          @conj try @refl >Hcl_val %2
     1575       | *: (* shr, translated to mod /!\ *)     
     1576          lapply (shr_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     1577          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
     1578          cases (sem_shr_inversion … Hsem_binary) normalize nodelta
     1579          #sz1 * #sz2 * #lhs_i * #rhs_i * * *
     1580          #Hcl_lhs #Hcl_rhs #Hshift_ok #Hcl_val
     1581          destruct (Hcl_lhs Hcl_rhs)
     1582          >(value_eq_int_inversion … Hvalue_eq_lhs)
     1583          >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
     1584          >Hshift_ok normalize nodelta >Hcl_val
     1585          /3 by ex_intro, conj, vint_eq/ ]
     1586     | *: (* comparison operators *)
     1587       lapply e' -e'
     1588       cases e1 #ed1 #ety1
     1589       cases e2 #ed2 #ety2
     1590       whd in match (typeof ?) in ⊢ (% → % → % → %);
     1591       #cm_expr whd in match (typeof ?);
     1592       inversion (classify_cmp ety1 ety2)
     1593       [ 3,6,9,12,15,18: #ety1' #ety2' #Hety1 #Hety2
     1594            lapply (jmeq_to_eq ??? Hety1) #Hety1'
     1595            lapply (jmeq_to_eq ??? Hety1) #Hety2'
     1596            destruct #Hclassify >Hclassify normalize nodelta
     1597            #cmexpr1 #cmexpr2
     1598            whd in ⊢ ((???%) → ?);
     1599            #Heq destruct (Heq)
     1600       | 1,4,7,10,13,16:
     1601            #sz #sg #Hety1 #Hety2 #Hclassify
     1602            lapply (jmeq_to_eq ??? Hety1) #Hety1'
     1603            lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
     1604            >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
     1605            whd in match (typeof ?) in ⊢ (% → % → % → %);
     1606            whd in match (typ_of_type ?) in ⊢ (% → % → ?);
     1607            cases sg #cmexpr1 #cmexpr2 normalize nodelta
     1608            #Hcast_to_bool #Hexec_expr
     1609            cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
     1610            #tysz * #tysg * #Htyis_int #Hcm_expr_aux
     1611            destruct (Htyis_int)
     1612            lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
     1613            destruct (Hcm_expr)
     1614            cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     1615            * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
     1616            cases (bind_inversion ????? Hexec) -Hexec
     1617            * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
     1618            cases (bind_inversion ????? Hexec) -Hexec
     1619            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1620            lapply (opt_to_res_inversion ???? Hsem) -Hsem
     1621            whd in match (typeof ?); whd in match (sem_binary_operation ??????);
     1622            #Hsem_cmp lapply (sem_cmp_int_inversion … Hsem_cmp) -Hsem_cmp
     1623            * #vsz * #lhs_val * #rhs_val * * #Hcl_lhs #Hcl_rhs normalize nodelta
     1624            destruct (Hcl_lhs) destruct (Hcl_rhs)
     1625            #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %);
     1626            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
     1627            * #Hyp_present_lhs #Hyp_present_rhs
     1628            #Hind_rhs #Hind_lhs                       
     1629            lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
     1630            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
     1631            lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
     1632            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
     1633            whd in match (eval_expr ???????);
     1634            whd in match (eval_expr ???????);
     1635            >Heval_lhs normalize nodelta
     1636            >Heval_rhs normalize nodelta
     1637            whd in match (m_bind ?????);
     1638            whd in match (eval_binop ???????);
     1639            >(value_eq_int_inversion … Hvalue_eq_lhs)
     1640            >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
     1641            >intsize_eq_elim_true normalize nodelta
     1642            destruct (Heq_bool)
     1643            whd in match (eval_unop ????);
     1644            whd in match (opt_to_res ???);
     1645            whd in match (m_bind ?????);
     1646            (* finished modulo glitch in integer widths *)
     1647            @cthulhu
     1648       | *:
     1649            #n #ty' #Hety1 #Hety2 #Hclassify
     1650            lapply (jmeq_to_eq ??? Hety1) #Hety1'
     1651            lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
     1652            >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
     1653            whd in match (typeof ?) in ⊢ (% → % → % → %);
     1654            #cmexpr1 #cmexpr2
     1655            #Hcast_to_bool #Hexec_expr
     1656            cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
     1657            #tysz * #tysg * #Htyis_int #Hcm_expr_aux
     1658            destruct (Htyis_int)
     1659            lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
     1660            destruct (Hcm_expr)
     1661            cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     1662            * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
     1663            cases (bind_inversion ????? Hexec) -Hexec
     1664            * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
     1665            cases (bind_inversion ????? Hexec) -Hexec
     1666            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1667            lapply (opt_to_res_inversion ???? Hsem) -Hsem
     1668            whd in match (typeof ?); whd in match (sem_binary_operation ??????);
     1669            #Hsem_cmp lapply (sem_cmp_ptr_inversion … Hsem_cmp) -Hsem_cmp
     1670            *
     1671            [ 2,4,6,8,10,12:
     1672              * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
     1673            | *: *
     1674              [ 2,4,6,8,10,12:
     1675                * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
     1676              | *: *
     1677                [ 2,4,6,8,10,12:
     1678                  * #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
     1679                | *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome destruct
     1680            ] ] ]
     1681           
     1682(*            #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %); *)
     1683            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
     1684            * #Hyp_present_lhs #Hyp_present_rhs
     1685            #Hind_rhs #Hind_lhs
     1686            lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)
     1687            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
     1688            lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)
     1689            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
     1690            whd in match (eval_expr ???????);
     1691            whd in match (eval_expr ???????);
     1692            >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
     1693            >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
     1694            whd in match (m_bind ?????);
     1695            -Heval_lhs -Heval_rhs -Hyp_present_rhs -Hyp_present_lhs
     1696            -Hexpr_vars_lhs -Hexpr_vars_rhs
     1697            whd in match (eval_binop ???????);
     1698            [ 1,2,3,4,5,6:
     1699              whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)           
     1700              >(value_eq_null_inversion … Hvalue_eq_lhs)
     1701              >(value_eq_null_inversion … Hvalue_eq_rhs) normalize nodelta
     1702              whd in match (eval_unop ????);
     1703              whd in match (opt_to_res ???);
     1704              whd in match (m_bind ?????);
     1705              (* same glitch with integer widths *)
     1706              @cthulhu
     1707            | 7,8,9,10,11,12:
     1708              whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)
     1709              >(value_eq_null_inversion … Hvalue_eq_lhs) normalize nodelta
     1710              cases (value_eq_ptr_inversion … Hvalue_eq_rhs) #p2'
     1711              * #Hcm_rhs_val #Hpointer_translation >Hcm_rhs_val normalize nodelta
     1712              whd in match (eval_unop ????);
     1713              whd in match (opt_to_res ???);
     1714              whd in match (m_bind ?????);
     1715              (* same glitch with integer widths *)
     1716              @cthulhu
     1717            | 13,14,15,16,17,18:
     1718              whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)
     1719              >(value_eq_null_inversion … Hvalue_eq_rhs) normalize nodelta
     1720              cases (value_eq_ptr_inversion … Hvalue_eq_lhs) #p1'
     1721              * #Hcm_lhs_val #Hpointer_translation >Hcm_lhs_val normalize nodelta
     1722              whd in match (eval_unop ????);
     1723              whd in match (opt_to_res ???);
     1724              whd in match (m_bind ?????);
     1725              (* same glitch with integer widths *)
     1726              @cthulhu
     1727            | *:
     1728              cases (value_eq_ptr_inversion … Hvalue_eq_lhs) #p1' * #Hcm_lhs #Hptr_translation_lhs
     1729              cases (value_eq_ptr_inversion … Hvalue_eq_rhs) #p2' * #Hcm_rhs #Hptr_translation_rhs
     1730              destruct (Hcm_lhs Hcm_rhs) normalize nodelta
     1731              -Hvalue_eq_lhs -Hvalue_eq_rhs -Hexec_lhs -Hexec_rhs
     1732              >(mi_valid_pointers … Hinj … Hvalid_p1 … Hptr_translation_lhs)
     1733              >(mi_valid_pointers … Hinj … Hvalid_p2 … Hptr_translation_rhs) normalize nodelta
     1734              lapply Heq_block_outcome -Heq_block_outcome
     1735              @(match eq_block (pblock p1) (pblock p2)
     1736                return λb. (eq_block (pblock p1) (pblock p2)) = b → ?
     1737                with
     1738                [ true ⇒ λH. ?
     1739                | false ⇒ λH. ?
     1740                ] (refl ? (eq_block (pblock p1) (pblock p2)))) normalize nodelta
     1741              [ 1,3,5,7,9,11:
     1742                 (* block equality in the Clight memory *)
     1743                 (* entails block equality in the Cminor memory *)
     1744                 >(pointer_translation_eq_block … Hptr_translation_lhs Hptr_translation_rhs H) normalize nodelta                 
     1745                 #Hsem_cmp whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)
     1746                 whd in match (eval_unop ????);
     1747                 whd in match (opt_to_res ???);
     1748                 whd in match (m_bind ?????);
     1749                 (* TODO !!! In order to finish this, we need an invariant on the fact that we don't blow the stack during
     1750                  * transformation *)
     1751                 @cthulhu
     1752              | *: (* TBF. In the case of block inequality, we will have to use the no_aliasing property of the memory injection. *)
     1753                 @cthulhu
     1754              ]
     1755            ]
     1756       ]
     1757 ]
    11321758     
    11331759| 1: (* Integer constant *)
Note: See TracChangeset for help on using the changeset viewer.