Changeset 1878


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

Enforce typing of constants in front-end, plus binops for RTLabs.

Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1872 r1878  
    337337(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
    338338| 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))))))
     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 Signed (repr ? (sizeof ty))))))
    340340| 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))))))
     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 Signed (repr ? (sizeof ty))))))
    342342| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
    343343].
     
    353353(* XXX could optimise cast as above *)
    354354| 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))))))
     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 Signed (repr ? (sizeof ty))))))
    356356(* XXX check in detail? *)
    357357| sub_case_pp n1 n2 r1 ty1 r2 ty2 ⇒
    358358    λ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))))))
     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 Signed (repr ? (sizeof ty2))))))
    360360    | _ ⇒ Error ? (msg TypeMismatch)
    361361    ]
     
    619619[ Expr ed ty ⇒
    620620  match ed with
    621   [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?»
    622   | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
     621  [ Econst_int sz i ⇒
     622      match ty return λty. res (Σe':CMexpr (typ_of_type ty).  expr_vars ? e' (local_id vars)) with
     623      [ Tint sz' sg ⇒ intsize_eq_elim' sz sz' (λsz,sz'. res (Σe':CMexpr (typ_of_type (Tint sz' sg)). expr_vars ? e' (local_id vars)))
     624                        (OK ? «Cst ? (Ointconst sz sg i), ?»)
     625                        (Error ? (msg TypeMismatch))
     626      | _ ⇒ Error ? (msg TypeMismatch)
     627      ]
     628  | Econst_float f ⇒
     629      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
     630      [ Tfloat sz ⇒ OK ? «Cst ? (Ofloatconst sz f), ?»
     631      | _ ⇒ Error ? (msg TypeMismatch)
     632      ]
    623633  | Evar id ⇒
    624634      do 〈c,t〉 as E ← lookup' vars id; (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *)
     
    632642           *)
    633643          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 *)
    635           | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
     644          [ By_value t ⇒ OK ? «Mem t r (Cst ? (Oaddrsymbol r id 0)), ?» (* Mem is "load" in compcert *)
     645          | By_reference r ⇒ OK ? «Cst ? (Oaddrsymbol r id 0), ?»
    636646          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    637647          ]
     
    641651          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
    642652          [ By_value t ⇒ OK ? «Mem t Any (Cst ? (Oaddrstack n)), ?»
    643           | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
     653          | By_reference r ⇒ match r return λr. res (Σe':CMexpr (ASTptr r). ?) with
     654                             [ Any ⇒ OK ? «Cst ? (Oaddrstack n), ?»
     655                             | _ ⇒ Error  ? [MSG BadlyTypedAccess; CTX ? id]
     656                             ]
    644657          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    645658          ]
     
    700713      do e1' ← translate_expr vars e1;
    701714      do e2' ← translate_expr vars e2;
    702       match ty with
    703       [ Tint sz _
    704         do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
     715      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
     716      [ Tint sz sg
     717        do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
    705718        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
    706         [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?»
     719        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz sg (zero ?))), ?»
    707720        | _ ⇒ λ_.Error ? (msg TypeMismatch)
    708721        ] e1'
     
    712725      do e1' ← translate_expr vars e1;
    713726      do e2' ← translate_expr vars e2;
    714       match ty with
    715       [ Tint sz _
    716         do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
     727      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
     728      [ Tint sz sg
     729        do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
    717730        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with
    718         [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?»
     731        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz sg (repr ? 1))) e2', ?»
    719732        | _ ⇒ λ_.Error ? (msg TypeMismatch)
    720733        ] e1'
     
    722735      ]
    723736  | Esizeof ty1 ⇒
    724       match ty with
    725       [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?»
     737      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
     738      [ Tint sz sg ⇒ OK ? «Cst ? (Ointconst sz sg (repr ? (sizeof ty1))), ?»
    726739      | _ ⇒ Error ? (msg TypeMismatch)
    727740      ]
     
    736749            [ By_value t ⇒
    737750                OK ? «Mem t r (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ?
    738                                    (Oaddp …) e1' (Cst ? (Ointconst I16 (repr ? off)))),?»
     751                                   (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off)))),?»
    739752            | By_reference r' ⇒
    740753                do e1' ← region_should_eq r r' ? e1';
    741754                OK ? «Op2 (ASTptr r') (ASTint I16 Signed (* XXX efficiency? *)) (ASTptr r')
    742                         (Oaddp …) e1' (Cst ? (Ointconst I16 (repr ? off))),?»
     755                        (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off))),?»
    743756            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
    744757            ]
     
    771784      do 〈c,t〉 ← lookup' vars id;
    772785      match c return λ_. res (𝚺r.Σz:CMexpr (ASTptr r).?) with
    773       [ Global r ⇒ OK ? ❬r, «Cst ? (Oaddrsymbol id 0), ?»❭
     786      [ Global r ⇒ OK ? ❬r, «Cst ? (Oaddrsymbol r id 0), ?»❭
    774787      | Stack n ⇒ OK ? ❬Any, «Cst ? (Oaddrstack n), ?»❭
    775788      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
     
    789802          [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)
    790803             (❬r, «Op2 (ASTptr r) (ASTint I16 Signed (* FIXME inefficient?*)) (ASTptr r)
    791                      (Oaddp I16 r) e1'' (Cst ? (Ointconst I16 (repr ? off))), ?» ❭)
     804                     (Oaddp I16 r) e1'' (Cst ? (Ointconst I16 Signed (repr ? off))), ?» ❭)
    792805          ]
    793806      | Tunion _ _ ⇒ translate_addr vars e1
     
    845858          match c return λx.? → ? with
    846859          [ Local ⇒ λE. OK ? (IdDest vars id t ?)
    847           | Global r ⇒ λE. OK ? (MemDest ? r (Cst ? (Oaddrsymbol id 0)))
     860          | Global r ⇒ λE. OK ? (MemDest ? r (Cst ? (Oaddrsymbol r id 0)))
    848861          | Stack n ⇒ λE. OK ? (MemDest ? Any (Cst ? (Oaddrstack n)))
    849862          ] E
  • src/Cminor/initialisation.ma

    r1872 r1878  
    99λinit.
    1010match init return λ_.option (𝚺t:typ. expr t) with
    11 [ Init_int8 i          ⇒ Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Cst ? (Ointconst I8 i)))
    12 | Init_int16 i         ⇒ Some ? (mk_DPair ?? (ASTint I16 Unsigned) (Cst ? (Ointconst I16 i)))
    13 | Init_int32 i         ⇒ Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Cst ? (Ointconst I32 i)))
    14 | Init_float32 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst f)))
    15 | Init_float64 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst f)))
     11[ Init_int8 i          ⇒ Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Cst ? (Ointconst I8 Unsigned i)))
     12| Init_int16 i         ⇒ Some ? (mk_DPair ?? (ASTint I16 Unsigned) (Cst ? (Ointconst I16 Unsigned i)))
     13| Init_int32 i         ⇒ Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Cst ? (Ointconst I32 Unsigned i)))
     14| Init_float32 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst F32 f)))
     15| Init_float64 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst F64 f)))
    1616| Init_space n         ⇒ None ?
    17 | Init_null r          ⇒ Some ? (mk_DPair ?? (ASTptr r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?)))))
    18 | Init_addrof r id off ⇒ Some ? (mk_DPair ?? (ASTptr r) (Cst ? (Oaddrsymbol id off)))
     17| Init_null r          ⇒ Some ? (mk_DPair ?? (ASTptr r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 Unsigned (zero ?)))))
     18| Init_addrof r id off ⇒ Some ? (mk_DPair ?? (ASTptr r) (Cst ? (Oaddrsymbol r id off)))
    1919].
    2020
     
    3535| Some x ⇒
    3636    match x with [ mk_DPair t e ⇒
    37       St_store t r (Cst ? (Oaddrsymbol id off)) e
     37      St_store t r (Cst ? (Oaddrsymbol r id off)) e
    3838    ]
    3939].
  • src/Cminor/semantics.ma

    r1874 r1878  
    9595    OK ? 〈E0, r〉
    9696| Cst _ c ⇒ λEnv.
    97     do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c);
     97    do r ← opt_to_res … (msg FailedConstant) (eval_constant ? (find_symbol … ge) sp c);
    9898    OK ? 〈E0, r〉
    9999| Op1 ty ty' op e' ⇒ λEnv.
  • src/Cminor/syntax.ma

    r1872 r1878  
    44include "basics/lists/list.ma".
    55
    6 (* TODO: consider making the typing stricter. *)
    7 
    86inductive expr : typ → Type[0] ≝
    97| Id : ∀t. ident → expr t
    10 | Cst : ∀t. constant → expr t
     8| Cst : ∀t. constant t → expr t
    119| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
    1210| Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
  • src/Cminor/toRTLabs.ma

    r1872 r1878  
    354354  statement_typed te s → statement_typed (〈r,t〉::te) s.
    355355#tw #r #t *
    356 [ 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
     356[ 3: #t' #r #cst #l #H %2 @H
     357| 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
     358| 5: #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
    357359| *: //
    358360] qed.
     
    517519    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
    518520    ]
    519 | Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const dst c) f ??, ?»
     521| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ??, ?»
    520522| Op1 t t' op e' ⇒ λEnv,dst.
    521523    let ❬f,r❭ ≝ choose_reg … e' f Env in
     
    556558try (#l @I)
    557559[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
    558 | 2,6,7: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
     560| #l @(pi2 … dst)
     561| 3,8,9: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
    559562| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
    560563| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
    561564| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
     565| #l % [ % [ @(fn_con_env ??????? (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I
    562566| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
    563567| @(π1 (π1 Env))
     
    752756      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
    753757      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
    754       let f ≝ add_fresh_to_graph … (St_op2 … (Ocmpu I8 Unsigned Ceq) (* signed? *) br r cr) f ?? in
    755       let f ≝ add_fresh_to_graph … (St_const cr (Ointconst ? i)) f ?? in
     758      let f ≝ add_fresh_to_graph … (St_op2 … (Ocmp sz sg Unsigned Ceq) br r cr) f ?? in
     759      let f ≝ add_fresh_to_graph … (St_const ? cr (Ointconst sz sg i)) f ?? in
    756760        OK ? «pi1 … f, ?») (OK ? f) tab;
    757761    OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»
     
    822826| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
    823827| #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I | @H ]
     828| #l % [ % [ @(fn_con_env … (pi2 ?? r)) | @(fn_con_env … (pi2 ?? cr)) ] | @(fn_con_env … (pi2 ?? br)) ] repeat @fn_contains_step @I
     829| #l @(fn_con_env … (pi2 ?? cr)) repeat @fn_contains_step @I
    824830| #_ (* see above *) <E @(pi2 ?? r)
    825831| @(pi2 … (pf_entry …))
  • src/RTLabs/semantics.ma

    r1874 r1878  
    9696  [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉
    9797  | St_cost cl l ⇒ λH. return 〈Echarge cl, build_state f fs m l ?〉
    98   | St_const r cst l ⇒ λH.
    99       ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
     98  | St_const _ r cst l ⇒ λH.
     99      ! v ← opt_to_res … (msg FailedConstant) (eval_constant ? (find_symbol … ge) (sp f) cst);
    100100      ! locals ← reg_store r v (locals f);
    101101      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     
    296296  [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
    297297  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
    298   | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
     298  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
    299299  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    300300  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
  • src/RTLabs/syntax.ma

    r1872 r1878  
    1212| St_skip : label → statement
    1313| St_cost : costlabel → label → statement
    14 | St_const : register → constant → label → statement
    15 | St_op1 : ∀t,t'. unary_operation t' t → register → register → label → statement (* destination source *)
    16 | St_op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → register → register → register → label → statement (* destination source1 source2 *)
     14| St_const : ∀t. register → constant t → label → statement
     15| St_op1 : ∀t',t. unary_operation t t' → register → register → label → statement (* destination source *)
     16| St_op2 : ∀t',t1,t2. binary_operation t1 t2 t' → register → register → register → label → statement (* destination source1 source2 *)
    1717| St_load : typ → register → register → label → statement
    1818| St_store : typ → register → register → label → statement
     
    3333definition statement_typed : list (register × typ) → statement → Prop ≝
    3434λe,s. match s with
    35 [ St_op1 t t' _ r r' _ ⇒ env_has e r t ∧ env_has e r' t'
     35[ St_const t r _ _ ⇒ env_has e r t
     36| St_op1 t' t _ r' r _ ⇒ env_has e r' t' ∧ env_has e r t
     37| St_op2 t' t1 t2 _ r' r1 r2 _ ⇒ env_has e r1 t1 ∧ env_has e r2 t2 ∧ env_has e r' t'
    3638| _ ⇒ True
    3739].
     
    4143[ St_skip l ⇒ P l
    4244| St_cost _ l ⇒ P l
    43 | St_const _ _ l ⇒ P l
     45| St_const _ _ _ l ⇒ P l
    4446| St_op1 _ _ _ _ _ l ⇒ P l
    4547| St_op2 _ _ _ _ _ _ _ l ⇒ P l
  • src/common/FrontEndOps.ma

    r1872 r1878  
    2020include "common/Values.ma".
    2121
    22 inductive constant : Type[0] ≝
    23   | Ointconst: ∀sz. bvint sz → constant    (**r integer constant *)
    24   | Ofloatconst: float → constant          (**r floating-point constant *)
    25   | Oaddrsymbol: ident → nat → constant    (**r address of the symbol plus the offset *)
    26   | Oaddrstack: nat → constant.            (**r stack pointer plus the given offset *)
     22inductive constant : typ → Type[0] ≝
     23  | Ointconst: ∀sz,sg. bvint sz → constant (ASTint sz sg)
     24  | Ofloatconst: ∀sz. float → constant (ASTfloat sz)
     25  | Oaddrsymbol: ∀r. ident → nat → constant (ASTptr r) (**r address of the symbol plus the offset *)
     26  | Oaddrstack: nat → constant (ASTptr Any).         (**r stack pointer plus the given offset *)
    2727
    2828definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr _ ⇒ True | _ ⇒ False ].
     
    7171
    7272
     73lemma elim_val_typ : ∀v,t. ∀P:val → Prop.
     74val_typ v t →
     75match t with
     76[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
     77| ASTfloat sz ⇒ ∀f.P (Vfloat f)
     78| ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o))
     79] →
     80P v.
     81#v #t #P *
     82[ 1,2: //
     83| #r * //
     84| #r #b #c #o * //
     85] qed.
     86
    7387(* * Evaluation of constants and operator applications.
    7488    [None] is returned when the computation is undefined, e.g.
     
    7690    by zero. *)
    7791
    78 definition eval_constant : (ident → option block) → block → constant → option val ≝
    79 λfind_symbol,sp,cst.
     92definition eval_constant : ∀t. (ident → option block) → block → constant t → option val ≝
     93λt,find_symbol,sp,cst.
    8094  match cst with
    81   [ Ointconst sz n ⇒ Some ? (Vint sz n)
    82   | Ofloatconst n ⇒ Some ? (Vfloat n)
    83   | Oaddrsymbol s ofs ⇒
     95  [ Ointconst sz sg n ⇒ Some ? (Vint sz n)
     96  | Ofloatconst sz n ⇒ Some ? (Vfloat n)
     97  | Oaddrsymbol r s ofs ⇒
    8498      match find_symbol s with
    8599      [ None ⇒ None ?
    86       | Some b ⇒ Some ? (Vptr (mk_pointer Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs))))
     100      | Some b ⇒ match pointer_compat_dec b r with
     101                 [ inl pc ⇒ Some ? (Vptr (mk_pointer r b pc (shift_offset ? zero_offset (repr I16 ofs))))
     102                 | inr _ ⇒ None ?
     103                 ]
    87104      ]
    88105  | Oaddrstack ofs ⇒
    89106      Some ? (Vptr (mk_pointer Any sp ? (shift_offset ? zero_offset (repr I16 ofs))))
    90107  ]. cases sp // qed.
     108
     109lemma eval_constant_typ_correct : ∀t,f,sp,c,v.
     110  eval_constant t f sp c = Some ? v →
     111  val_typ v t.
     112#t #f #sp *
     113[ #sz #sg #i #v #E normalize in E; destruct //
     114| #sz #f #v #E normalize in E; destruct //
     115| #r #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct
     116  cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct
     117  //
     118| #n #v #E whd in E:(??%?); destruct //
     119] qed.
    91120
    92121definition eval_unop : ∀t,t'. unary_operation t t' → val → option val ≝
     
    119148  | Ointofptr sz sg r ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    120149  ].
    121 
    122 lemma elim_val_typ : ∀v,t. ∀P:val → Prop.
    123 val_typ v t →
    124 match t with
    125 [ ASTint sz sg ⇒ ∀i.P (Vint sz i)
    126 | ASTfloat sz ⇒ ∀f.P (Vfloat f)
    127 | ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o))
    128 ] →
    129 P v.
    130 #v #t #P *
    131 [ 1,2: //
    132 | #r * //
    133 | #r #b #c #o * //
    134 ] qed.
    135150
    136151lemma eval_unop_typ_correct : ∀t,t',op,v,v'.
Note: See TracChangeset for help on using the changeset viewer.