Changeset 961 for src/Cminor


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

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

Location:
src/Cminor
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r887 r961  
    99λinit.
    1010match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with
    11 [ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst i)))
    12 | Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst i)))
    13 | Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst i)))
     11[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
     12| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
     13| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst I32 i)))
    1414| Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
    1515| Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
    1616| Init_space n         ⇒ None ?
    17 | Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst zero))))
     17| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst I8 (zero ?)))))
    1818| Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
    1919].
     
    2222   away. *)
    2323
    24 definition init_datum : ident → region → init_data → int (*offset?*) → stmt ≝
     24definition init_datum : ident → region → init_data → nat (*offset*) → stmt ≝
    2525λid,r,init,off.
    2626match init_expr init with
     
    3737  (λdatum,os.
    3838   let 〈off,s〉 ≝ os in
    39      〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id r datum off) s〉)
    40   〈zero, St_skip〉 init).
     39     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
     40  〈0, St_skip〉 init).
    4141
    4242definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
  • src/Cminor/semantics.ma

    r886 r961  
    9191].
    9292
    93 let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝
     93let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝
    9494match cs with
    9595[ nil ⇒ default
    9696| cons h t ⇒
    9797    let 〈hi,a〉 ≝ h in
    98     if eq i hi then a else find_case A i t default
     98    if eq_bv ? i hi then a else find_case A sz i t default
    9999].
    100100
     
    199199        ! k' ← k_exit n k;
    200200        ret ? 〈E0, State f St_skip en m sp k'〉
    201     | St_switch _ _ e cs default ⇒
     201    | St_switch sz _ e cs default ⇒
    202202        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    203203        match v with
    204         [ Vint i ⇒
    205             ! k' ← k_exit (find_case ? i cs default) k;
    206             ret ? 〈tr, State f St_skip en m sp k'〉
     204        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
     205            ! k' ← k_exit (find_case ?? i cs default) k;
     206            ret ? 〈tr, State f St_skip en m sp k'〉)
     207            (Wrong ??? (msg BadSwitchValue))
    207208        | _ ⇒ Wrong ??? (msg BadSwitchValue)
    208209        ]
     
    257258        | Some v ⇒
    258259            match v with
    259             [ Vint i ⇒ Some ? i
     260            [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
    260261            | _ ⇒ None ?
    261262            ]
  • src/Cminor/syntax.ma

    r886 r961  
    2727| St_exit : nat → stmt
    2828(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
    29 | St_switch : ∀sz,sg. expr (ASTint sz sg) → list (int × nat) → nat → stmt
     29| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
    3030| St_return : option (Σt. expr t) → stmt
    3131| St_label : ident → stmt → stmt
  • src/Cminor/toRTLabs.ma

    r888 r961  
    210210      do f ← add_fresh_to_graph (St_cond br l_case) f;
    211211      do f ← add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f;
    212       add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
     212      add_fresh_to_graph (St_const cr (Ointconst ? i)) f) (OK ? f) tab;
    213213    add_expr env ? e r f
    214214| St_return opt_e ⇒
Note: See TracChangeset for help on using the changeset viewer.