Changeset 1988 for src/Clight


Ignore:
Timestamp:
May 24, 2012, 11:39:27 AM (8 years ago)
Author:
campbell
Message:

Abstraction of the memory contents in the memory models is no longer
necessary.

Location:
src/Clight
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1986 r1988  
    294294| cons h vars ⇒
    295295  let 〈id,ty〉 ≝ h in
    296   let 〈m1,b1〉 ≝ alloc becontentT m 0 (sizeof ty) Any in
     296  let 〈m1,b1〉 ≝ alloc 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 becontentT m (blocks_of_env e))〉
     382          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list 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 becontentT m (blocks_of_env e))〉
     387          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list 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 becontentT m (blocks_of_env e))〉
     448      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list 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 becontentT m (blocks_of_env e))〉
     456          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
    457457        ]
    458458    ]
  • src/Clight/CexecSound.ma

    r1876 r1988  
    349349[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
    350350| * #id #ty #t #IH #en #m #en' #m'
    351   lapply (refl ? (alloc ? m O (sizeof ty) Any)) #ALLOC #EXEC
     351  lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
    352352  whd in EXEC:(??%?) ALLOC:(???%);
    353353 @(alloc_variables_cons … ALLOC)
  • src/Clight/Csem.ma

    r1986 r1988  
    526526  | alloc_variables_cons:
    527527      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    528       alloc becontentT m 0 (sizeof ty) Any = 〈m1, b1〉 →
     528      alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
    529529      alloc_variables (add … e id (pi1 … b1)) m1 vars e2 m2 →
    530530      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
     
    11391139      fn_return f = Tvoid →
    11401140      step ge (State f (Sreturn (None ?)) k e m)
    1141            E0 (Returnstate Vundef (call_cont k) (free_list becontentT m (blocks_of_env e)))
     1141           E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e)))
    11421142  | step_return_1: ∀f,a,k,e,m,v,tr.
    11431143      fn_return f ≠ Tvoid →
    11441144      eval_expr ge e m a v tr →
    11451145      step ge (State f (Sreturn (Some ? a)) k e m)
    1146            tr (Returnstate v (call_cont k) (free_list becontentT m (blocks_of_env e)))
     1146           tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
    11471147  | step_skip_call: ∀f,k,e,m.
    11481148      is_call_cont k →
    11491149      fn_return f = Tvoid →
    11501150      step ge (State f Sskip k e m)
    1151            E0 (Returnstate Vundef k (free_list becontentT m (blocks_of_env e)))
     1151           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
    11521152
    11531153  | step_switch: ∀f,a,sl,k,e,m,sz,n,tr.
  • src/Clight/test/memorymodel.ma

    r1875 r1988  
    2020   access, preventing you reading back more information than the memory can
    2121   store. *)
    22 definition store0 := empty becontentT.
    23 definition store1block : mem × Σb:block.? ≝ alloc ? store0 0 4 Any.
     22definition store0 := empty.
     23definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 Any.
    2424definition store1 : mem ≝ fst ?? store1block.
    2525definition block :block := pi1 … (snd ?? store1block).
     
    5151(* NB: Double frees are allowed by the memory model (although not necessarily
    5252       by the language). *)
    53 definition store4 := free ? store3 block.
    54 definition store5 : mem. letin r ≝ (free ? store3 block); whd in r; @r qed.
     53definition store4 := free store3 block.
     54definition store5 : mem. letin r ≝ (free store3 block); whd in r; @r qed.
    5555
    5656(* No ordering is imposed on deallocation (even though alloc and free are only used for
    5757   stack memory in the semantics. *)
    58 definition storeA := empty becontentT.
    59 definition storeBblkB := alloc ? storeA 0 4 Any.
    60 definition storeCblkC := alloc ? (fst ?? storeBblkB) 0 8 Any.
    61 definition storeD := free ? (fst ?? storeCblkC) (snd ?? storeBblkB).
    62 definition storeE : mem. letin r ≝ (free ? storeD (snd ?? storeCblkC)).
     58definition storeA := empty.
     59definition storeBblkB := alloc storeA 0 4 Any.
     60definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
     61definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
     62definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
    6363whd in r; @r qed.
    6464
     
    6666   but can now split up integer values into bytes.  The front-end interface
    6767   doesn't currently expose parts of pointers. *)
    68 definition storeI := empty becontentT.
    69 definition storeIIblk := alloc ? storeA 0 4 Any.
     68definition storeI := empty.
     69definition storeIIblk := alloc storeI 0 4 Any.
    7070definition storeIII : mem.
    7171 letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset) (Vint I32 (repr ? 1)));
Note: See TracChangeset for help on using the changeset viewer.