Ignore:
Timestamp:
Apr 4, 2012, 6:48:23 PM (8 years ago)
Author:
campbell
Message:

Make binary operations in Cminor/RTLabs properly typed.
A few extra bits and pieces that help:
Separate out Clight operation classification to its own file.
Use dependently typed classification to refine the types.
Fix bug in cast simplification.
Remove memory_chunk in favour of the low-level typ, as this now contains
exactly the right amount of information (unlike in CompCert?).
Make Cminor/RTLabs comparisons produce an 8-bit result (and cast if
necessary).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1871 r1872  
    1 include "Clight/Csyntax.ma".
    2 include "Clight/TypeComparison.ma".
     1include "Clight/ClassifyOp.ma".
    32include "basics/lists/list.ma".
    43include "Clight/fresh.ma".
     
    322321  Consistency of the type is enforced by explicit checks.
    323322*)
     323
     324(* First, how to get rid of a abstract-away pointer or array type *)
     325definition fix_ptr_type : ∀r,ty,n. expr (typ_of_type (ptr_type r ty n)) → expr (ASTptr r) ≝
     326λr,ty,n,e. e⌈expr (typ_of_type (ptr_type r ty n)) ↦ expr (ASTptr r)⌉.
     327cases n //
     328qed.
     329
    324330definition translate_add ≝
    325 λty1,e1,ty2,e2,ty'.
     331λty1,ty2,ty'.
    326332let ty1' ≝ typ_of_type ty1 in
    327333let ty2' ≝ typ_of_type ty2 in
    328 match classify_add ty1 ty2 with
    329 [ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
    330 | add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
    331 (* XXX using the integer size for e2 as the offset's size isn't right, because
    332    if e2 produces an 8bit value then the true offset might overflow *)
    333 | add_case_pi ty ⇒
    334     match ty2' with
    335     [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty))))))
    336     | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
    337     ]
    338 | add_case_ip ty ⇒
    339     match ty1' with
    340     [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty))))))
    341     | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
    342     ]
    343 | add_default ⇒ Error ? (msg TypeMismatch)
     334match classify_add ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     335[ add_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd ??) e1 e2)
     336| add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2)
     337(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
     338| add_case_pi n r ty sz sg ⇒
     339    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
     340| add_case_ip n sz sg r ty ⇒
     341    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
     342| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
    344343].
    345344
    346345
    347346definition translate_sub ≝
    348 λty1,e1,ty2,e2,ty'.
     347λty1,ty2,ty'.
    349348let ty1' ≝ typ_of_type ty1 in
    350349let ty2' ≝ typ_of_type ty2 in
    351 match classify_sub ty1 ty2 with
    352 [ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
    353 | sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
    354 (* XXX choosing offset sizes? *)
    355 | sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
    356 | sub_case_pp ty ⇒
    357     match ty' with (* XXX overflow *)
    358     [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty)))))
    359     | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
    360     ]
    361 | sub_default ⇒ Error ? (msg TypeMismatch)
     350match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     351[ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2)
     352| sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2)
     353(* XXX could optimise cast as above *)
     354| sub_case_pi n r ty sz sg ⇒
     355    λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
     356(* XXX check in detail? *)
     357| sub_case_pp n1 n2 r1 ty1 r2 ty2 ⇒
     358    λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with
     359    [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16 r1 r2) (fix_ptr_type … e1) (fix_ptr_type ??? e2)) (Cst ? (Ointconst I16 (repr ? (sizeof ty2))))))
     360    | _ ⇒ Error ? (msg TypeMismatch)
     361    ]
     362| sub_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    362363].
    363364
    364365definition translate_mul ≝
    365 λty1,e1,ty2,e2,ty'.
     366λty1,ty2,ty'.
    366367let ty1' ≝ typ_of_type ty1 in
    367368let ty2' ≝ typ_of_type ty2 in
    368 match classify_mul ty1 ty2 with
    369 [ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
    370 | mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
    371 | mul_default ⇒ Error ? (msg TypeMismatch)
     369match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     370[ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omul …) e1 e2)
     371| aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omulf …) e1 e2)
     372| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    372373].
    373374
    374375definition translate_div ≝
    375 λty1,e1,ty2,e2,ty'.
     376λty1,ty2,ty'.
    376377let ty1' ≝ typ_of_type ty1 in
    377378let ty2' ≝ typ_of_type ty2 in
    378 match classify_div ty1 ty2 with
    379 [ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
    380 | div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
    381 | div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
    382 | div_default ⇒ Error ? (msg TypeMismatch)
     379match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     380[ aop_case_ii sz sg ⇒
     381    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
     382    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivu …) e1 e2)
     383    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odiv …) e1 e2)
     384    ]
     385| aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivf …) e1 e2)
     386| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    383387].
    384388
    385389definition translate_mod ≝
    386 λty1,e1,ty2,e2,ty'.
     390λty1,ty2,ty'.
    387391let ty1' ≝ typ_of_type ty1 in
    388392let ty2' ≝ typ_of_type ty2 in
    389 match classify_mod ty1 ty2 with
    390 [ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
    391 | mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
    392 | mod_default ⇒ Error ? (msg TypeMismatch)
     393match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     394[ aop_case_ii sz sg ⇒
     395    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
     396    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2)
     397    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2)
     398    ]
     399(* no float case *)
     400| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    393401].
    394402
    395403definition translate_shr ≝
    396 λty1,e1,ty2,e2,ty'.
     404λty1,ty2,ty'.
    397405let ty1' ≝ typ_of_type ty1 in
    398406let ty2' ≝ typ_of_type ty2 in
    399 match classify_shr ty1 ty2 with
    400 [ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
    401 | shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
    402 | shr_default ⇒ Error ? (msg TypeMismatch)
     407match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     408[ aop_case_ii sz sg ⇒
     409    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
     410    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2)
     411    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2)
     412    ]
     413(* no float case *)
     414| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
     415].
     416
     417definition complete_cmp : ∀ty'. CMexpr (ASTint I8 Unsigned) → res (CMexpr (typ_of_type ty')) ≝
     418λty',e.
     419match ty' return λty'. res (CMexpr (typ_of_type ty')) with
     420[ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I8 Unsigned sz sg) e)
     421| _ ⇒ Error ? (msg TypeMismatch)
    403422].
    404423
    405424definition translate_cmp ≝
    406 λc,ty1,e1,ty2,e2,ty'.
     425λc,ty1,ty2,ty'.
    407426let ty1' ≝ typ_of_type ty1 in
    408427let ty2' ≝ typ_of_type ty2 in
    409 match classify_cmp ty1 ty2 with
    410 [ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2)
    411 | cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2)
    412 | cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2)
    413 | cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2)
    414 | cmp_default ⇒ Error ? (msg TypeMismatch)
     428match classify_cmp ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     429[ cmp_case_ii sz sg ⇒
     430    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
     431    [ Unsigned ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpu … c) e1 e2)
     432    | Signed ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmp … c) e1 e2)
     433    ]
     434| cmp_case_pp n r ty ⇒
     435    λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpp … c) (fix_ptr_type … e1) (fix_ptr_type … e2))
     436| cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2)
     437| cmp_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
     438].
     439
     440definition translate_misc_aop ≝
     441λty1,ty2,ty',op.
     442let ty1' ≝ typ_of_type ty1 in
     443let ty2' ≝ typ_of_type ty2 in
     444match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     445[ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ?? (ASTint sz sg) (op sz sg) e1 e2)
     446| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    415447].
    416448
     
    419451let ty' ≝ typ_of_type ty in
    420452match op with
    421 [ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty'
    422 | Osub ⇒ translate_sub ty1 e1 ty2 e2 ty'
    423 | Omul ⇒ translate_mul ty1 e1 ty2 e2 ty'
    424 | Omod ⇒ translate_mod ty1 e1 ty2 e2 ty'
    425 | Odiv ⇒ translate_div ty1 e1 ty2 e2 ty'
    426 | Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2)
    427 | Oor  ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2)
    428 | Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2)
    429 | Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2)
    430 | Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty'
    431 | Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty'
    432 | One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty'
    433 | Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty'
    434 | Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty'
    435 | Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty'
    436 | Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty'
    437 ].
     453[ Oadd ⇒ translate_add ty1 ty2 ty e1 e2
     454| Osub ⇒ translate_sub ty1 ty2 ty e1 e2
     455| Omul ⇒ translate_mul ty1 ty2 ty e1 e2
     456| Omod ⇒ translate_mod ty1 ty2 ty e1 e2
     457| Odiv ⇒ translate_div ty1 ty2 ty e1 e2
     458| Oand ⇒ translate_misc_aop ty1 ty2 ty Oand e1 e2
     459| Oor  ⇒ translate_misc_aop ty1 ty2 ty Oor e1 e2
     460| Oxor ⇒ translate_misc_aop ty1 ty2 ty Oxor e1 e2
     461| Oshl ⇒ translate_misc_aop ty1 ty2 ty Oshl e1 e2
     462| Oshr ⇒ translate_shr ty1 ty2 ty e1 e2
     463| Oeq ⇒ translate_cmp Ceq ty1 ty2 ty e1 e2
     464| One ⇒ translate_cmp Cne ty1 ty2 ty e1 e2
     465| Olt ⇒ translate_cmp Clt ty1 ty2 ty e1 e2
     466| Ogt ⇒ translate_cmp Cgt ty1 ty2 ty e1 e2
     467| Ole ⇒ translate_cmp Cle ty1 ty2 ty e1 e2
     468| Oge ⇒ translate_cmp Cge ty1 ty2 ty e1 e2
     469].
     470
     471lemma typ_equals : ∀t1,t2. ∀P:∀t. expr t → Prop. ∀v1,v2.
     472  typ_should_eq t1 t2 expr v1 = OK ? v2 →
     473  P t1 v1 →
     474  P t2 v2.
     475* [ * * | * | * ]
     476* try * try *
     477#P #v1 #v2 #E whd in E:(??%?); destruct
     478#H @H
     479qed.
     480
     481lemma unfix_ptr_type : ∀r,ty,n,e.∀P:∀t. expr t → Prop.
     482  P (typ_of_type (ptr_type r ty n)) e →
     483  P (ASTptr r) (fix_ptr_type r ty n e).
     484#r #ty * [ 2: #n ] #e #P #H @H
     485qed.
    438486
    439487(* Recall that [expr_vars], defined in Cminor/Syntax.ma, asserts a predicate on
     
    442490  a proof that all variables of [translate_binop op _ e1 _ e2 _] satisfy this
    443491  predicate. *)
     492
    444493lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
    445494  expr_vars ? e1 P →
     
    449498#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
    450499whd in ⊢ (??%? → ?);
    451 [ cases (classify_add ty1 ty2)
    452   [ 3,4: #z ] whd in ⊢ (??%? → ?);
    453   [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    454     * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    455     whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
    456   | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    457     * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    458     whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
    459   | *: #E destruct (E) % try @H1 @H2
     500[ inversion (classify_add ty1 ty2) in ⊢ ?;
     501  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 -E3 change with (typ_should_eq ???? = OK ??) in E4;
     502    @(typ_equals … E4) % //
     503  | #sz #E1 #E2 #E3 destruct >E3 #E4
     504    @(typ_equals … E4) % //
     505  | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
     506    @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ]
     507  | #n #sz #sg #r #ty0 #E1 #E2 #E3 destruct >E3 #E4
     508    @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2)| % // ]
     509  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    460510  ]
    461 | cases (classify_sub ty1 ty2)
    462   [ 3,4: #z] whd in ⊢ (??%? → ?);
    463   [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    464     * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    465     whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
    466   | *: #E destruct (E) % try @H1 try @H2 % // @H2
     511| inversion (classify_sub ty1 ty2) in ⊢ ?;
     512  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4
     513    @(typ_equals … E4) % //
     514  | #sz #E1 #E2 #E3 destruct >E3 #E4
     515    @(typ_equals … E4) % //
     516  | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
     517    @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ]
     518  | #n1 #n2 #r1 #ty1' #r2 #ty2' #E1 #E2 #E3 destruct >E3
     519    whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
     520    [ 2: #sz #sg #e #E4 | 4: #r #ty #e #E4 | 5: #r #ty' #n' #e #E4
     521    | *: normalize #X1 #X2 try #X3 try #X4 destruct
     522    ] whd in E4:(??%?); destruct % // %
     523    [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1) | @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2) ]
     524  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    467525  ]
    468 | cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct
    469     % try @H1 @H2
    470 | cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct
    471     % try @H1 @H2
    472 | cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct
    473     % try @H1 @H2
    474 | 6,7,8,9: #E destruct % try @H1 @H2
    475 | cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
    476 | 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
     526| 3,4,5,6,7,8,9,10: inversion (classify_aop ty1 ty2) in ⊢ ?;
     527  (* Note that some cases require a split on signedness of integer type. *)
     528  [ 1,4,7,10,13,16,19,22: #sz * #E1 #E2 #E3 destruct >E3 #E4
     529    @(typ_equals … E4) % //
     530  | 2,5: #sz #E1 #E2 #E3 destruct >E3 #E4
     531    @(typ_equals … E4) % //
     532  | 8,11,14,17,20,23: #sz #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
     533  | 3,6,9,12,15,18,21,24: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
     534  ]
     535| 11,12,13,14,15,16: inversion (classify_cmp ty1 ty2) in ⊢ ?;
     536  [ 1,5,9,13,17,21: #sz * #E1 #E2 #E3 destruct >E3
     537  | 2,6,10,14,18,22: #n #r #ty' #E1 #E2 #E3 destruct >E3
     538  | 3,7,11,15,19,23: #sz #E1 #E2 #E3 destruct >E3
     539  | *: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); @⊥ destruct
     540  ] whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
     541  try (normalize #X1 #X2 try #X3 try #X4 try #X5 destruct #FAIL)
     542  #sz #sg #e #E4
     543  whd in E4:(??%?); destruct %
     544  [ 25,27,29,31,33,35: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)
     545  | 26,28,30,32,34,36: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2)
     546  | *: //
     547  ]
    477548] qed.
     549
    478550
    479551(* We'll need to implement proper translation of pointers if we really do memory
     
    532604]. whd normalize nodelta @pi2
    533605qed.
    534 
    535 (* Small inversion lemma : if the access mode of a type is by reference, then it must be a ptr type. *)
    536 lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
    537 *
    538 [ 5: #r #ty #n #r' normalize #E destruct @refl
    539 | 6: #args #ret #r normalize #E destruct @refl
    540 | *: normalize #a #b try #c try #d destruct
    541   [ cases a in d; normalize; cases b; normalize #E destruct
    542   | cases a in c; normalize #E destruct
    543   ]
    544 ] qed.
    545606
    546607(* Translate Clight exprs into Cminor ones.
     
    570631             - By_nothing : error
    571632           *)
    572           match access_mode ty with
    573           [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)
     633          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
     634          [ By_value t ⇒ OK ? «Mem t r (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)
    574635          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
    575           | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
     636          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    576637          ]
    577638      | Stack n ⇒ λE.
    578639          (* We have decided that the variable should be allocated on the stack,
    579640           * because its adress was taken somewhere or becauste it's a structured data. *)
    580           match access_mode ty with
    581           [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?»
     641          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
     642          [ By_value t ⇒ OK ? «Mem t Any (Cst ? (Oaddrstack n)), ?»
    582643          | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
    583           | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
     644          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    584645          ]
    585646          (* This is a local variable. Keep it as an identifier in the Cminor code, ensuring that the type of the original expr and of ty match. *)
     
    596657      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
    597658      [ ASTptr r ⇒ λe1'.
    598           match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with
    599           [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (pi1 … e1'), ?»
    600           | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1';
    601                                   OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉
    602           | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
    603           ] (access_mode_typ ty)
     659          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
     660          [ By_value t ⇒ OK ? «Mem t ? (pi1 … e1'), ?»
     661          | By_reference r' ⇒ region_should_eq r r' ? e1'
     662          | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
     663          ]
    604664      | _ ⇒ λ_. Error ? (msg TypeMismatch)
    605665      ] e1'
     
    673733          [ mk_DPair r e1' ⇒
    674734            do off ← field_offset id fl;
    675             match access_mode ty with
    676             [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?»
    677             | By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?»
    678             | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
     735            match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
     736            [ By_value t ⇒
     737                OK ? «Mem t r (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ?
     738                                   (Oaddp …) e1' (Cst ? (Ointconst I16 (repr ? off)))),?»
     739            | By_reference r' ⇒
     740                do e1' ← region_should_eq r r' ? e1';
     741                OK ? «Op2 (ASTptr r') (ASTint I16 Signed (* XXX efficiency? *)) (ASTptr r')
     742                        (Oaddp …) e1' (Cst ? (Ointconst I16 (repr ? off))),?»
     743            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
    679744            ]
    680745          ]
     
    683748          match e1' with
    684749          [ mk_DPair r e1' ⇒
    685             match access_mode ty return λx. access_mode ty = x → res ? with
    686             [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?»
    687             | By_reference r' ⇒  λE. do e1' ← region_should_eq r r' ? e1';
    688                                 OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉
    689             | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
    690             ] (refl ? (access_mode ty))
     750            match access_mode ty return λt.λ_. res (Σz:CMexpr t.?) with
     751            [ By_value t ⇒ OK ? «Mem t ? e1', ?»
     752            | By_reference r' ⇒ region_should_eq r r' ? e1'
     753            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
     754            ]
    691755          ]
    692756      | _ ⇒ Error ? (msg BadlyTypedAccess)
     
    723787          do off ← field_offset id fl;
    724788          match e1' with
    725           [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?) (❬r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» ❭)
     789          [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)
     790             (❬r, «Op2 (ASTptr r) (ASTint I16 Signed (* FIXME inefficient?*)) (ASTptr r)
     791                     (Oaddp I16 r) e1'' (Cst ? (Ointconst I16 (repr ? off))), ?» ❭)
    726792          ]
    727793      | Tunion _ _ ⇒ translate_addr vars e1
     
    733799whd try @I
    734800[ >E whd @refl
    735 | >(E ? (refl ??)) @refl
    736 | 3,4: @pi2
     801| 2,3: @pi2
    737802| @(translate_binop_vars … E) @pi2
    738803| % [ % ] @pi2
     
    741806| % [ @pi2 | @I ]
    742807| % [ @pi2 | @I ]
    743 | >(access_mode_typ … E) @refl
    744808| @pi2
    745809| @pi2
     
    747811] qed.
    748812
     813(* We provide a function to work out how to do an assignment to an lvalue
     814   expression.  It is used for both Clight assignments and Clight function call
     815   destinations, but doesn't take the value to be assigned so that we can use
     816   it to form a single St_store when possible (and avoid introducing an
     817   unnecessary temporary variable and assignment).
     818   *)
    749819inductive destination (vars:var_types) : Type[0] ≝
    750820| IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars
    751 | MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
     821| MemDest : ∀r:region. (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
    752822
    753823(* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a
     
    767837*)
    768838definition translate_dest ≝
    769 λvars,e1,ty2.
    770     do q ← match access_mode ty2 with
    771            [ By_value q ⇒ OK ? q
    772            | By_reference r ⇒ OK ? (Mpointer r)
    773            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
    774            ];
    775     match e1 with
    776     [ Expr ed1 ty1 ⇒
    777         match ed1 with
    778         [ Evar id ⇒
    779             do 〈c,t〉 as E ← lookup' vars id;
    780             match c return λx.? → ? with
    781             [ Local ⇒ λE. OK ? (IdDest vars id t ?)
    782             | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0)))
    783             | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n)))
    784             ] E
    785         | _ ⇒
    786             do e1' ← translate_addr vars e1;
    787             match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r q e1') ]
    788         ]
    789     ].
     839λvars,e1.
     840  match e1 with
     841  [ Expr ed1 ty1 ⇒
     842      match ed1 with
     843      [ Evar id ⇒
     844          do 〈c,t〉 as E ← lookup' vars id;
     845          match c return λx.? → ? with
     846          [ Local ⇒ λE. OK ? (IdDest vars id t ?)
     847          | Global r ⇒ λE. OK ? (MemDest ? r (Cst ? (Oaddrsymbol id 0)))
     848          | Stack n ⇒ λE. OK ? (MemDest ? Any (Cst ? (Oaddrstack n)))
     849          ] E
     850      | _ ⇒
     851          do e1' ← translate_addr vars e1;
     852          match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r e1') ]
     853      ]
     854  ].
    790855whd // >E @refl
    791856qed.
     
    884949definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt. stmt_inv vars s) ≝
    885950λvars,e1,e2.
    886 do e2' ← translate_expr vars e2;             
    887 do dest ← translate_dest vars e1 (typeof e2);
     951do e2' ← translate_expr vars e2;
     952do dest ← translate_dest vars e1;
    888953match dest with
    889954[ IdDest id ty p ⇒
    890955    do e2' ← type_should_eq (typeof e2) ty ? e2';
    891956    OK ? «St_assign ? id e2', ?»
    892 | MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
     957| MemDest r e1' ⇒ OK ? «St_store ? r e1' e2', ?»
    893958].
    894959% try (//)  try (elim e2' //) elim e1' //
     
    10461111[ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?»
    10471112| Sassign e1 e2 ⇒
    1048     do e2' ← translate_expr vars e2;              (* rhs *)
    1049     do dest ← translate_dest vars e1 (typeof e2); (* e1 *)
     1113    do e2' ← translate_expr vars e2;  (* rhs *)
     1114    do dest ← translate_dest vars e1; (* e1 *)
    10501115    match dest with
    10511116    [ IdDest id ty p ⇒
    10521117       do e2' ← type_should_eq (typeof e2) ty ? e2';
    10531118       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
    1054     | MemDest r q e1' ⇒
    1055        OK ? «〈uv, ul, St_store ? r q e1' e2'〉, ?»
     1119    | MemDest r e1' ⇒
     1120       OK ? «〈uv, ul, St_store ? r e1' e2'〉, ?»
    10561121    ]
    10571122| Scall ret ef args ⇒
     
    10621127    [ None ⇒ OK ? «〈uv, ul, St_call (None ?) ef' args'〉, ?»
    10631128    | Some e1 ⇒
    1064         do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
     1129        do dest ← translate_dest vars e1;
    10651130        match dest with
    10661131        [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
    1067         | MemDest r q e1' ⇒
     1132        | MemDest r e1' ⇒
    10681133            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
    1069             OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r q e1' (Id ? tmp))〉, ?»
     1134            OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r e1' (Id ? tmp))〉, ?»
    10701135        ]
    10711136    ]
     
    13641429  [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is»
    13651430  | Stack n ⇒ λE.
    1366       do q ← match access_mode ty with
    1367       [ By_value q ⇒ OK ? q
    1368       | By_reference r ⇒ OK ? (Mpointer r)
    1369       | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    1370       ];
    1371       OK ? «〈fgens1, St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
     1431      OK ? «〈fgens1, St_seq (St_store ? Any (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
    13721432  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
    13731433  ] E) (OK ? s) params.
Note: See TracChangeset for help on using the changeset viewer.