Ignore:
Timestamp:
Mar 8, 2013, 12:48:20 PM (7 years ago)
Author:
garnier
Message:

A consitent proof state for Clight to Cminor, with some progress (and some temporary regressions)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2686 r2822  
    701701        - if e1 is a struct* or a function ptr, then we acess by reference, in which case we :
    702702           1) check the consistency of the regions in the type of e1 and in the access mode of its type
    703            2) return directly the converted CMinor expression "as is" (TODO : what is the strange notation with the ceil function and the mapsto ?)
     703           2) return directly the converted CMinor expression "as is"
    704704      *)
    705705      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
     
    11841184       do e2' ← typ_should_eq (typ_of_type (typeof e2)) (typ_of_type ty) ? e2';
    11851185       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
    1186     | MemDest e1' ⇒
    1187        OK ? «〈uv, ul, St_store ? e1' e2'〉, ?»
     1186    | MemDest e1' ⇒
     1187       match type_eq_dec (typeof e1) (typeof e2) with
     1188       [ inl Hcl_typ_eq ⇒       
     1189         OK ? «〈uv, ul, St_store ? e1' e2'〉, ?»
     1190       | inr Hcl_typ_neq ⇒
     1191         Error ? (msg TypeMismatch)
     1192       ]
    11881193    ]
    11891194| Scall ret ef args ⇒
     
    11961201        do dest ← translate_dest vars e1;
    11971202        match dest with
    1198         [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
     1203        [ IdDest id ty p ⇒
     1204            (* No trace generated here, by inversion on translate_dest _ _ = IdDest _ _ _ *)
     1205            OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
    11991206        | MemDest e1' ⇒
    12001207            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
    1201             OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) e1' (Id ? tmp))〉, ?»
     1208            (* alloc a new variable to serve as a placeholder for the evaluation of e1',
     1209             * which /must/ happen before the call. Otherwise, the cost labels are not
     1210             * emitted as in Clight.  *)
     1211            let 〈tmp2, uv2〉 as Etmp' ≝ alloc_tmp ? (Tpointer (typeof e1)) uv1 in
     1212            OK ? «〈uv2, ul,
     1213                    (St_seq (St_store ? (Id ? tmp2) e1')
     1214                    (St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args')
     1215                            (St_store (typ_of_type (typeof e1)) e1' (Id ? tmp))))〉, ?»
    12021216        ]
    12031217    ]
     
    13361350try (#H1 try #H2 assumption)
    13371351[ 1,5: @(tmp_preserved … p) ]
    1338 [ 1,3: elim e2' | 2,9,23: elim e1' | 4,7,13: elim ef' ]
    1339 [ 1,2,3,4,5,6,7,8 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
    1340 [ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
     1352[ 6: @(local_id_fresh_tmp vars tmp2 uv2 (Tpointer (typeof e1)) uv1 Etmp')
     1353| 7: cases e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1354| 8: @conj try @conj normalize nodelta
     1355     [ 1: cases e1' #e #Hvars lapply (local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp)
     1356          @(alloc_tmp_preserves … Etmp')
     1357     | 3: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
     1358                  | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
     1359                  | 3: elim args' // ]
     1360     | 2: cases ef' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ] ]
     1361[ 5: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
    13411362             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
    1342              | 3: elim args' // ]
    1343 | 7: (* we should be able to merge this case with the previous ... *)
    1344      @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
     1363             | 3: elim args' // ] ]
     1364[ 5: whd @conj
     1365     [ 1: cases e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1366     | 2: @(alloc_tmp_preserves … Etmp') @(local_id_fresh_tmp … Etmp) ] ]     
     1367[ 1,3: elim e2' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1368| 2: elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1369| 4,7: elim ef' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
     1370[ 3: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
    13451371             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
    13461372             | 3: elim args' // ]
    1347 | 2: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp)
    1348 | 3:  @(All_mp (𝚺 t:typ.expr t) (λe. match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars)]))
    1349        [ 1: #a #Ha elim a in Ha ⊢ ?; #ta #a #Ha whd @(expr_vars_mp ?? (local_id vars))
    1350        [ 1: #i0 #t0 #H0 @(tmp_preserved vars uv1 i0 t0 H0)
    1351        | 2: assumption ]
    1352        | 2: elim args' // ]
    1353 | 4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ]
    1354 [ 1: #size #sign | 2: ]
    1355 [ 1,2: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
     1373| 2: #H @(alloc_tmp_preserves … Etmp' l ASTptr) @(alloc_tmp_preserves … Etmp l ASTptr) @H
     1374| 1: #sz #sg #H @(alloc_tmp_preserves … Etmp' l) @(alloc_tmp_preserves … Etmp l) @H ]
    13561375try @refl (* Does (at least) the return_ok cases *)
    13571376try @(match fgens1 return λx.x=fgens1 → ? with
     
    13671386try (elim H2 -H2 * * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2 #Hret2)
    13681387try (elim H3 -H3 * * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3 #Hret3)
     1388[ 8: whd cases e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
    13691389[ 1,2: #Hind1 #Hind2 | 3,4,8,10: #Hind | 5: #Hind1 #Hind2 #Hind3 ]
    13701390try @conj try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
Note: See TracChangeset for help on using the changeset viewer.