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.

File:
1 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
Note: See TracChangeset for help on using the changeset viewer.