Changeset 1874 for src/common/Mem.ma


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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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*)
Note: See TracChangeset for help on using the changeset viewer.