Changeset 1874


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

First cut at using back-end memory model throughout.
Note the correction to BEValues.

Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1713 r1874  
    294294| cons h vars ⇒
    295295  let 〈id,ty〉 ≝ h in
    296   let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) Any in
     296  let 〈m1,b1〉 ≝ alloc becontentT m 0 (sizeof ty) Any in
    297297      exec_alloc_variables (add ?? en id b1) m1 vars
    298298].
     
    380380      | Kstop ⇒
    381381          match fn_return f with
    382           [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
     382          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list becontentT m (blocks_of_env e))〉
    383383          | _ ⇒ Wrong ??? (msg NonsenseState)
    384384          ]
    385385      | Kcall _ _ _ _ ⇒
    386386          match fn_return f with
    387           [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
     387          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list becontentT m (blocks_of_env e))〉
    388388          | _ ⇒ Wrong ??? (msg NonsenseState)
    389389          ]
     
    446446    match a_opt with
    447447    [ None ⇒ match fn_return f with
    448       [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
     448      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list becontentT m (blocks_of_env e))〉
    449449      | _ ⇒ Wrong ??? (msg ReturnMismatch)
    450450      ]
     
    454454        | inr _ ⇒
    455455          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    456           ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
     456          ret ? 〈tr, Returnstate v (call_cont k) (free_list becontentT m (blocks_of_env e))〉
    457457        ]
    458458    ]
  • src/Clight/Csem.ma

    r1872 r1874  
    526526  | alloc_variables_cons:
    527527      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    528       alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
    529       alloc_variables (add … e id b1) m1 vars e2 m2 →
     528      alloc becontentT m 0 (sizeof ty) Any = 〈m1, b1〉 →
     529      alloc_variables (add … e id (pi1 … b1)) m1 vars e2 m2 →
    530530      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    531531
     
    11371137      fn_return f = Tvoid →
    11381138      step ge (State f (Sreturn (None ?)) k e m)
    1139            E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e)))
     1139           E0 (Returnstate Vundef (call_cont k) (free_list becontentT m (blocks_of_env e)))
    11401140  | step_return_1: ∀f,a,k,e,m,v,tr.
    11411141      fn_return f ≠ Tvoid →
    11421142      eval_expr ge e m a v tr →
    11431143      step ge (State f (Sreturn (Some ? a)) k e m)
    1144            tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
     1144           tr (Returnstate v (call_cont k) (free_list becontentT m (blocks_of_env e)))
    11451145  | step_skip_call: ∀f,k,e,m.
    11461146      is_call_cont k →
    11471147      fn_return f = Tvoid →
    11481148      step ge (State f Sskip k e m)
    1149            E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
     1149           E0 (Returnstate Vundef k (free_list becontentT m (blocks_of_env e)))
    11501150
    11511151  | step_switch: ∀f,a,sl,k,e,m,sz,n,tr.
  • src/Cminor/semantics.ma

    r1872 r1874  
    300300        | Kblock k' ⇒ λkInv. return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    301301          (* cminor allows functions without an explicit return statement *)
    302         | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
     302        | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free ? m sp) st〉
    303303        ] kInv
    304304    | St_assign _ id e ⇒ λInv.
     
    345345    | St_return eo ⇒
    346346        match eo return λeo. stmt_inv f en (St_return eo) → ? with
    347         [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
     347        [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free ? m sp) st〉
    348348        | Some e ⇒
    349349            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv.
    350350              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    351               return 〈tr, Returnstate (Some ? v) (free m sp) st〉
     351              return 〈tr, Returnstate (Some ? v) (free ? m sp) st〉
    352352            ]
    353353        ]
     
    363363    match fd with
    364364    [ Internal f ⇒ err_to_io ?? (trace × state) (
    365         let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
     365        let 〈m',sp〉 ≝ alloc ? m 0 (f_stacksize f) Any in
    366366        ! en ← bind_params args (f_params f);
    367367        return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉)
  • src/RTLabs/semantics.ma

    r1872 r1874  
    167167                return (Some ? v)
    168168            ];
    169       return 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
     169      return 〈E0, Returnstate v (retdst f) fs (free ? m (sp f))〉
    170170  ] (f_closed (func f) (next f) s ?)
    171171| Callstate fd params dst fs m ⇒
     
    175175        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
    176176           here *)
    177         let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
     177        let 〈m', sp〉 ≝ alloc ? m 0 (f_stacksize fn) Any in
    178178        return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
    179179    | External fn ⇒
     
    313313| * #fn #args #retdst #stk #m #tr #s'
    314314  whd in ⊢ (??%? → ?);
    315   [ @bind_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
     315  [ @bind_value #loc #Eloc cases (alloc ? m O ??) #m' #b whd in ⊢ (??%? → ?);
    316316    #E destruct %3
    317317  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
  • src/common/FrontEndVal.ma

    r1873 r1874  
    11include "common/Values.ma".
    22include "joint/BEValues.ma".
    3 include "common/Mem.ma".
    43
    54(* Transform between lists of "back-end" (i.e., byte by byte) values and the
     
    76   resolve the sizes; they are not strictly checked. *)
    87
    9 let rec make_parts (r:region) (n:nat) (H:le n (size_pointer r)) on n : list (part r) ≝
    10 match n return λn.le n ? → ? with
    11 [ O ⇒ λ_. [ ]
    12 | S m ⇒ λH'. mk_part r n H::(make_parts r m ?)
     8let rec make_parts_aux (r:region) (n:nat) (H:lt n (size_pointer r)) (tl:list (part r)) on n : list (part r) ≝
     9match n return λn.lt n ? → ? with
     10[ O ⇒ λH'. (mk_part r O H')::tl
     11| S m ⇒ λH'. make_parts_aux r m ? ((mk_part r n H)::tl)
    1312] H.
    1413/2/
    1514qed.
    1615
    17 definition make_be_null : region → list beval
    18 λr. map ?? (λp. BVnull r p) (make_parts r (size_pointer r) ?).
     16definition make_parts : ∀r:region. list (part r)
     17λr. make_parts_aux r (pred (size_pointer r)) ? [ ].
    1918//
    2019qed.
     20
     21definition make_be_null : region → list beval ≝
     22λr. map ?? (λp. BVnull r p) (make_parts r).
    2123
    2224let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝
  • src/common/Globalenvs.ma

    r1872 r1874  
    404404     addresses of the memory region in question - here there are no real
    405405     pointers, so use the real region. *)
    406   let r ≝ block_region m b in
     406  let ptr ≝ mk_pointer (block_region ? m b) b ? (mk_offset p) in
    407407  match id with
    408   [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m r b p (Vint I8 n)
    409   | Init_int16 n ⇒ store (ASTint I16 Unsigned) m r b p (Vint I16 n)
    410   | Init_int32 n ⇒ store (ASTint I32 Unsigned) m r b p (Vint I32 n)
    411   | Init_float32 n ⇒ store (ASTfloat F32) m r b p (Vfloat n)
    412   | Init_float64 n ⇒ store (ASTfloat F64) m r b p (Vfloat n)
     408  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
     409  | Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n)
     410  | Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n)
     411  | Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n)
     412  | Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n)
    413413  | Init_addrof r' symb ofs ⇒
    414414      match (*find_symbol ge symb*) symbols ? ge symb with
     
    416416      | Some b' ⇒
    417417        match pointer_compat_dec b' r' with
    418         [ inl pc ⇒ store (ASTptr r') m r b p (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
     418        [ inl pc ⇒ store (ASTptr r') m ptr (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
    419419        | inr _ ⇒ None ?
    420420        ]
    421421      ]
    422422  | Init_space n ⇒ Some ? m
    423   | Init_null r' ⇒ store (ASTptr r') m r b p (Vnull r')
     423  | Init_null r' ⇒ store (ASTptr r') m ptr (Vnull r')
    424424  ].
     425cases b //
     426qed.
    425427
    426428definition size_init_data : init_data → nat ≝
     
    471473*)
    472474
     475(* TODO: why doesn't this use alloc? *)
    473476definition alloc_init_data : mem → list init_data → region → mem × block ≝
    474477  λm,i_data,r.
    475   let b ≝ mk_block r (nextblock m) in
    476   〈mk_mem (update_block ? b
    477                  (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef))
    478                  (blocks m))
    479          (Zsucc (nextblock m))
    480          (succ_nextblock_pos m),
     478  let b ≝ mk_block r (nextblock ? m) in
     479  〈mk_mem ? (update_block ? b
     480                 (mk_block_contents becontentT OZ (size_init_data_list i_data) (λ_.BVundef))
     481                 (blocks ? m))
     482         (Zsucc (nextblock ? m))
     483         (succ_nextblock_pos ? m),
    481484   b〉.
    482485
     
    520523λF,V,init_info,p.
    521524  add_globals … init_info
    522    〈add_functs ? (empty …) (prog_funct F ? p), empty_mem
     525   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem ?
    523526   (prog_vars ?? p).
    524527
  • src/common/Mem.ma

    r1872 r1874  
     1include "joint/BEMem.ma".
     2include "common/FrontEndVal.ma".
     3
     4definition mem ≝ bemem.
     5
     6let rec loadn (m:bemem) (ptr:pointer) (n:nat) on n : option (list beval) ≝
     7match n with
     8[ O ⇒ Some ? ([ ])
     9| S n' ⇒
     10  match beloadv m ptr with
     11  [ None ⇒ None ?
     12  | Some v ⇒ match loadn m (shift_pointer 2 ptr (bitvector_of_nat … 1)) n' with
     13             [ None ⇒ None ?
     14             | Some vs ⇒ Some ? (v::vs) ]
     15  ]
     16].
     17
     18definition load : typ → mem → pointer → option val ≝
     19λt,m,ptr.
     20  match loadn m ptr (typesize t) with
     21  [ None ⇒ None ?
     22  | Some vs ⇒ Some ? (be_to_fe_value t vs)
     23  ].
     24
     25let rec loadv (t:typ) (m:bemem) (addr:val) on addr : option val ≝
     26match addr with
     27[ Vptr ptr ⇒ load t m ptr
     28| _ ⇒ None ?
     29].
     30
     31let rec storen (m:bemem) (ptr:pointer) (vs:list beval) on vs : option bemem ≝
     32match vs with
     33[ nil ⇒ Some ? m
     34| cons v tl ⇒
     35  match bestorev m ptr v with
     36  [ None ⇒ None ?
     37  | Some m' ⇒ storen m' (shift_pointer 2 ptr (bitvector_of_nat … 1)) tl
     38  ]
     39].
     40
     41definition store : typ → bemem → pointer → val → option bemem ≝
     42λt,m,ptr,v. storen m ptr (fe_to_be_values t v).
     43
     44definition storev : typ → bemem → val → val → option bemem ≝
     45λt,m,addr,v.
     46  match addr with
     47  [ Vptr ptr ⇒ store t m ptr v
     48  | _ ⇒ None ? ].
     49
     50(* Only used by Clight semantics for pointer comparisons.  So in contrast to
     51   CompCert, we allow a pointer-to-one-off-the-end. *)
     52
     53definition valid_pointer : mem → pointer → bool ≝
     54λm,ptr. Zltb (block_id (pblock ptr)) (nextblock ? m) ∧
     55  Zleb (low_bound ? m (pblock ptr)) (offv (poff ptr)) ∧
     56  Zleb (offv (poff ptr)) (high_bound ? m (pblock ptr)).
     57
     58
     59(*
    160(* *********************************************************************)
    261(*                                                                     *)
     
    35183577qed.
    35193578*)
     3579*)
  • src/joint/BEValues.ma

    r1601 r1874  
    66record part (r: region): Type[0] ≝
    77 { part_no:> nat
    8  ; part_no_ok: part_no size_pointer r
     8 ; part_no_ok: part_no < size_pointer r
    99 }.
    1010
Note: See TracChangeset for help on using the changeset viewer.