Changeset 961 for src/Clight/toCminor.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r886 r961  
    141141match ls with
    142142[ LSdefault s1 ⇒ gather_mem_vars_stmt s1
    143 | LScase _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
    144                     gather_mem_vars_ls ls1
     143| LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
     144                      gather_mem_vars_ls ls1
    145145].
    146146
     
    217217[ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
    218218| add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
    219 | add_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst (repr (sizeof ty))))))
    220 | add_case_ip ty ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst (repr (sizeof ty))))))
     219(* XXX using the integer size for e2 as the offset's size isn't right, because
     220   if e2 produces an 8bit value then the true offset might overflow *)
     221| add_case_pi ty ⇒
     222    match ty2' with
     223    [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty))))))
     224    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
     225    ]
     226| add_case_ip ty ⇒
     227    match ty1' with
     228    [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty))))))
     229    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
     230    ]
    221231| add_default ⇒ Error ? (msg TypeMismatch)
    222232].
     
    229239[ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
    230240| sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
    231 | sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst (repr (sizeof ty))))))
    232 | sub_case_pp ty ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' Osubpp e1 e2) (Cst ? (Ointconst (repr (sizeof ty)))))
     241(* XXX choosing offset sizes? *)
     242| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
     243| sub_case_pp ty ⇒
     244    match ty' with (* XXX overflow *)
     245    [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty)))))
     246    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
     247    ]
    233248| sub_default ⇒ Error ? (msg TypeMismatch)
    234249].
     
    249264let ty2' ≝ typ_of_type ty2 in
    250265match classify_div ty1 ty2 with
    251 [ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2) (* FIXME: should be 8 bit only *)
     266[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
    252267| div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
    253268| div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
     
    260275let ty2' ≝ typ_of_type ty2 in
    261276match classify_mod ty1 ty2 with
    262 [ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2) (* FIXME: should be 8 bit only *)
     277[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
    263278| mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
    264279| mod_default ⇒ Error ? (msg TypeMismatch)
     
    270285let ty2' ≝ typ_of_type ty2 in
    271286match classify_shr ty1 ty2 with
    272 [ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2) (* FIXME: should be 8 bit only *)
     287[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
    273288| shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
    274289| shr_default ⇒ Error ? (msg TypeMismatch)
     
    331346[ Tint sz1 sg1 ⇒ λe.
    332347    match ty2 return λx.res (CMexpr (typ_of_type x)) with
    333     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME: do we need to do zero/sign ext?  Ought to be 8 bit anyway... *)
     348    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sz2 sg2) e)
    334349    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
    335350    | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
     
    339354| Tfloat sz1 ⇒ λe.
    340355    match ty2 return λx.res (CMexpr (typ_of_type x)) with
    341     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat | _ ⇒ Ointoffloat]) e)
     356    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e)
    342357    | Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME *)
    343358    | _ ⇒ Error ? (msg TypeMismatch)
     
    345360| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
    346361    match ty2 return λx.res (CMexpr (typ_of_type x)) with
    347     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? Ointofptr e)
     362    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ointofptr sz2) e)
    348363    | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
    349364    | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
     
    352367| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
    353368    match ty2 return λx.res (CMexpr (typ_of_type x)) with
    354     [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) Ointofptr e)
     369    [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e)
    355370    | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
    356371    | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
     
    393408[ Expr ed ty ⇒
    394409  match ed with
    395   [ Econst_int i ⇒ OK ? (Cst ? (Ointconst i))
     410  [ Econst_int sz i ⇒ OK ? (Cst ? (Ointconst sz i))
    396411  | Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))
    397412  | Evar id ⇒
     
    400415      [ Global r ⇒
    401416          match access_mode ty with
    402           [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id zero)))
    403           | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id zero))
     417          [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id 0)))
     418          | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id 0))
    404419          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    405420          ]
    406421      | Stack n ⇒
    407422          match access_mode ty with
    408           [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack (repr n))))
    409           | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack (repr n)))
     423          [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack n)))
     424          | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack n))
    410425          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    411426          ]
     
    457472      do e1' ← translate_expr vars e1;
    458473      do e2' ← translate_expr vars e2;
    459       do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
    460       match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    461       [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst zero)))
    462       | _ ⇒ λ_.Error ? (msg TypeMismatch)
    463       ] e1'
     474      match ty with
     475      [ Tint sz _ ⇒
     476        do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
     477        match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
     478        [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))))
     479        | _ ⇒ λ_.Error ? (msg TypeMismatch)
     480        ] e1'
     481      | _ ⇒ Error ? (msg TypeMismatch)
     482      ]
    464483  | Eorbool e1 e2 ⇒
    465484      do e1' ← translate_expr vars e1;
    466485      do e2' ← translate_expr vars e2;
    467       do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
    468       match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    469       [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst one)) e2')
    470       | _ ⇒ λ_.Error ? (msg TypeMismatch)
    471       ] e1'
    472   | Esizeof ty1 ⇒ OK ? (Cst ? (Ointconst (repr (sizeof ty1))))
     486      match ty with
     487      [ Tint sz _ ⇒
     488        do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
     489        match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
     490        [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2')
     491        | _ ⇒ λ_.Error ? (msg TypeMismatch)
     492        ] e1'
     493      | _ ⇒ Error ? (msg TypeMismatch)
     494      ]
     495  | Esizeof ty1 ⇒
     496      match ty with
     497      [ Tint sz _ ⇒ OK ? (Cst ? (Ointconst sz (repr ? (sizeof ty1))))
     498      | _ ⇒ Error ? (msg TypeMismatch)
     499      ]
    473500  | Efield e1 id ⇒
    474501      do e' ← match typeof e1 with
     
    479506            do off ← field_offset id fl;
    480507            match access_mode ty with
    481             [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off)))))
    482             | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off))))
     508            [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
     509            | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))
    483510            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
    484511            ]
     
    509536      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    510537      match c return λ_. res (Σr.CMexpr (ASTptr r)) with
    511       [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id zero)))
    512       | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack (repr n))))
     538      [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))
     539      | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n)))
    513540      | Local ⇒ Error ? (msg BadlyTypedAccess) (* TODO: could rule out? *)
    514541      ]
     
    525552          do off ← field_offset id fl;
    526553          match e1' with
    527           [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst (repr off)))))
     554          [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
    528555          ]
    529556      | Tunion _ _ ⇒ translate_addr vars e1
     
    554581            match c with
    555582            [ Local ⇒ OK ? (IdDest id)
    556             | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id zero)))
    557             | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack (repr n))))
     583            | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id 0)))
     584            | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack n)))
    558585            ]
    559586        | _ ⇒
Note: See TracChangeset for help on using the changeset viewer.