Changeset 1415 for src/joint


Ignore:
Timestamp:
Oct 19, 2011, 4:22:52 PM (9 years ago)
Author:
sacerdot
Message:
  1. hwreg_store/retrieve no longer returns a res (but it is still axiomatized)
  2. added initialization of local environment that sets the sp in the appropriate way
  3. ASM/I8051 splitted into ASM/I8051bis because of some bugs with disambiguation
Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1408 r1415  
    1515axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
    1616axiom empty_hw_register_env: hw_register_env.
    17 axiom hwreg_retrieve : hw_register_env → Register → res beval.
    18 axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env.
     17axiom hwreg_retrieve : hw_register_env → Register → beval.
     18axiom hwreg_store : Register → beval → hw_register_env → hw_register_env.
     19
     20definition init_hw_register_env: address → hw_register_env ≝
     21 λaddr.
     22  let 〈dpl,dph〉 ≝ addr in
     23  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
     24   hwreg_store RegisterDPL dpl env.
    1925
    2026(****************************************************************************)
  • src/joint/semantics.ma

    r1411 r1415  
    44include "common/SmallstepExec.ma".
    55include "joint/Joint.ma".
     6include "ASM/I8051bis.ma".
    67
    78(* CSC: external functions never fail (??) and always return something of the
     
    1415 ; empty_framesT: framesT
    1516 ; regsT: Type[0]
    16  ; empty_regsT: regsT
     17 ; empty_regsT: address → regsT (* Stack pointer *)
    1718 ; call_args_for_main: call_args p
    1819 ; call_dest_for_main: call_dest p
     
    396397  let ge ≝ genv2 sem_globals in
    397398  let m ≝ init_mem Genv … p in
    398   let dummy_pc ≝ 〈BVundef,BVundef〉 in
    399   let sp ≝ ? in
     399  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
     400  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
     401  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
     402  do sp ← address_of_pointer spp ;
    400403  let main ≝ prog_main … p in
    401   let st0 ≝ mk_state … (empty_framesT …) dummy_pc sp BVfalse (empty_regsT …) m in
     404  let st0 ≝ mk_state … (empty_framesT …) sp dummy_pc BVfalse (empty_regsT … sp) m in
    402405  let trace_state ≝
    403406   eval_call_id … (mk_sem_params1 … (sparams …)) ge st0 main (call_args_for_main … (sparams …))
     
    408411  | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    409412  ].
    410 cases daemon qed.
     413[2: % | cases spb *; #r #off #E >E %]
     414qed.
    411415(*
    412416RTL:
Note: See TracChangeset for help on using the changeset viewer.