Changeset 1381 for src/RTL

Timestamp:

Oct 14, 2011, 10:29:54 PM (9 years ago)

Author:

sacerdot

Message:

Old commented out code removed.

File:

• src/RTL/semantics.ma (modified) (2 diffs)

src/RTL/semantics.ma

@@ -1 +1 @@
 include "joint/SemanticUtils.ma".
-(*
-include "utilities/lists.ma".
-include "common/Errors.ma".
-include "common/Globalenvs.ma".
-include "common/IO.ma".
-include "common/SmallstepExec.ma".
-*)
 include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
 include alias "common/Identifiers.ma".
@@ -123 +116 @@
 definition rtl_fullexec ≝
  joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
-
-(*
-(* CSC: external functions never fail (??) and always return something of the
-   size of one register, both in the frontend and in the backend.
-   Is this reasonable??? In OCaml it always return a list, but in the frontend
-   only the head is kept (or Undef if the list is empty) ??? *)
-
-(* CSC: carries are values and booleans are not values; so we use integers.
-   But why using values at all? To have undef? *)
-(* CSC: ???????????? *)
-axiom smerge: val → val → res val.
-(* CSC: ???????????? In OCaml: IntValue.Int32.merge
-   Note also that the translation can fail; so it should be a res int! *)
-axiom smerge2: list val → int.
-(* CSC: I have a byte, I need a value, but it is complex to do so *)
-axiom val_of_Byte: Byte → val.
-axiom Byte_of_val: val → res Byte.
-(* Map from the front-end memory model to the back-end memory model *)
-axiom represent_block: block → val × val.
-(* CSC: fixed size chunk *)
-axiom chunk: memory_chunk.
-
-definition genv ≝ (genv_t Genv) (fundef rtl_internal_function).
-
-(* CSC: added carry *)
-record frame : Type[0] ≝
-{ func   : rtl_internal_function
-; locals : register_env val
-; next   : label
-; sp     : block
-; retdst : list register
-; carry  : val
-}.
-
-(* CSC: added carry *)
-definition adv : label → frame → frame ≝
-λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f) (carry f).
-
-inductive state : Type[0] ≝
-| State : 
-   ∀   f : frame.
-   ∀  fs : list frame.
-   ∀   m : mem.
-   state
-| Callstate :
-   ∀  fd : fundef rtl_internal_function.
-   ∀args : list val.
-   ∀ dst : list register. (* CSC: changed from option to list *)
-   ∀ stk : list frame.
-   ∀   m : mem.
-   state
-| Returnstate :
-   (* CSC: the two lists should have the same length, but this is
-      enforced only by the semantics *)
-   ∀ rtv : list val. (* CSC: changed from option to list *)
-   ∀ dst : list register. (* CSC: changed from option to list *)
-   ∀ stk : list frame.
-   ∀   m : mem.
-   state.
-
-definition mem_of_state : state → mem ≝
-λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
-
-definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
-
-(* CSC: modified to take in input a list of registers (untyped) *)
-definition init_locals : list register → register_env val ≝
-foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
-
-definition reg_store ≝
-λreg,v,locals.
-  update RegisterTag val locals reg v.
-
-axiom WrongNumberOfParameters : String.
-
-(* CSC: modified to take in input a list of registers (untyped) *)
-let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
-match rs with
-[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
-| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
-  let locals' ≝ add RegisterTag val locals r v in
-  params_store rst vst locals'
-] ].
-
-axiom BadRegister : String.
-
-definition reg_retrieve : register_env ? → register → res val ≝
-λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
-
-axiom FailedOp : String.
-axiom MissingSymbol : String.
-
-axiom MissingStatement : String.
-axiom FailedConstant : String.
-axiom FailedLoad : String.
-axiom FailedStore : String.
-axiom BadFunction : String.
-axiom BadJumpTable : String.
-axiom BadJumpValue : String.
-axiom FinalState : String.
-axiom ReturnMismatch : String.
-
-definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
-λge,st.
-match st with
-[ State f fs m ⇒
-  ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (rtl_if_graph (func f)) (next f)); 
-  match s with
-  [ rtl_st_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
-  | rtl_st_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
-  | rtl_st_load addrl addrh dst l ⇒  (* CSC: pairs of regs vs reg *)
-      ! vaddrh ← reg_retrieve (locals f) addrh;
-      ! vaddrl ← reg_retrieve (locals f) addrl;
-      ! vaddr ← smerge vaddrl vaddrh;
-      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
-      ! locals ← reg_store dst v (locals f);
-      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
-  | rtl_st_store addrl addrh src l ⇒  (* CSC: pairs of regs vs reg *)
-      ! vaddrh ← reg_retrieve (locals f) addrh;
-      ! vaddrl ← reg_retrieve (locals f) addrl;
-      ! vaddr ← smerge vaddrl vaddrh;
-      ! v ← reg_retrieve (locals f) src;
-      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
-      ret ? 〈E0, build_state f fs m' l〉
-  | rtl_st_call_id id args dst l ⇒
-      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
-      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
-      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
-      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
-  | rtl_st_call_ptr lfrs hfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
-      ! hfv ← reg_retrieve (locals f) hfrs;
-      ! lfv ← reg_retrieve (locals f) lfrs;
-      ! fv  ← smerge lfv hfv;
-      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
-      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
-      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
-  | rtl_st_tailcall_id id args ⇒
-      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
-      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
-      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
-      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
-  | rtl_st_tailcall_ptr lfrs hfrs args ⇒ (* CSC: pairs of regs vs reg *)
-      ! hfv ← reg_retrieve (locals f) hfrs;
-      ! lfv ← reg_retrieve (locals f) lfrs;
-      ! fv  ← smerge lfv hfv;
-      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
-      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
-      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
-  | rtl_st_return ⇒
-      (* CSC: rtl_if_result/f_result; list vs option *)
-      let dest ≝ rtl_if_result (func f) in
-      ! v ←  mmap … (reg_retrieve (locals f)) dest;
-      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
-  | rtl_st_cond src ltrue lfalse ⇒
-      ! v ← reg_retrieve (locals f) src;
-      ! b ← eval_bool_of_val v;
-      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
-  (* CSC: mismatch between the memory models and failures for the next two opx *)
-  | rtl_st_op1 op dst src l ⇒
-     ! v ← reg_retrieve (locals f) src;
-     ! v ← Byte_of_val v;
-     let v' ≝ val_of_Byte (op1 eval op v) in
-     ! locals ← reg_store dst v' (locals f);
-     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉 
-  | rtl_st_op2 op dst src1 src2 l ⇒
-     ! v1 ← reg_retrieve (locals f) src1;
-     ! v1 ← Byte_of_val v1;
-     ! v2 ← reg_retrieve (locals f) src2;
-     ! v2 ← Byte_of_val v2;
-     ! carry ← eval_bool_of_val (carry f);
-     let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
-     let v' ≝ val_of_Byte v' in
-     let carry ≝ of_bool carry in
-     ! locals ← reg_store dst v' (locals f);
-     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) carry) fs m〉 
-
-  (* CSC: Removed: St_jumptable *)
-  (* CSC: Added: *)
-  
-  (* CSC: St_const splitted into rtl_st_int, rtl_st_addr and rt_st_stack_addr; *)
-  | rtl_st_addr ldest hdest id l ⇒
-     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
-     let 〈laddr,haddr〉 ≝ represent_block addr in
-     ! locals ← reg_store ldest laddr (locals f);
-     ! locals ← reg_store hdest haddr locals;
-     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
-  | rtl_st_stack_addr ldest hdest l ⇒
-     let 〈laddr,haddr〉 ≝ represent_block (sp f) in
-     ! locals ← reg_store ldest laddr (locals f);
-     ! locals ← reg_store hdest haddr locals;
-     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
-  | rtl_st_int dest v l ⇒
-     ! locals ← reg_store dest (val_of_Byte v) (locals f);
-     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
-
-  (* CSC: St_op1 splitted into rtl_st_op1 and rtl_st_move *)
-  | rtl_st_move dst src l ⇒
-     ! v ← reg_retrieve (locals f) src;
-     ! locals ← reg_store dst v (locals f);
-     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉 
-  (* CSC: St_op2 splitted into rtl_st_op2 and rtl_st_opaccs *)  
-  | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒
-     ! v1 ← reg_retrieve (locals f) sacc;
-     ! v1 ← Byte_of_val v1;
-     ! v2 ← reg_retrieve (locals f) sbacc;
-     ! v2 ← Byte_of_val v2;
-     let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
-     let v1' ≝ val_of_Byte v1' in
-     let v2' ≝ val_of_Byte v2' in
-     ! locals ← reg_store dacc v1' (locals f);
-     ! locals ← reg_store dbacc v2' locals;
-     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉 
-  
-  | rtl_st_clear_carry l ⇒
-    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vfalse) fs m〉
-  | rtl_st_set_carry l ⇒
-    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
-  ]
-| Callstate fd params dst fs m ⇒
-    match fd with
-    [ Internal fn ⇒
-        ! locals ← params_store (rtl_if_params fn) params (init_locals (rtl_if_locals fn));
-        let 〈m', sp〉 ≝ alloc m 0 (rtl_if_stacksize fn) Any in
-        (* CSC: added carry *)
-        ret ? 〈E0, State (mk_frame fn locals (rtl_if_entry fn) sp dst Vundef) fs m'〉
-    | External fn ⇒
-        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
-        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
-        (* CSC: return type changed from option to list *)
-        (* CSC: XXX bug here; I think I should split it into Byte-long
-           components; instead I am making a singleton out of it *)
-        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
-    ]
-| Returnstate v dst fs m ⇒
-    match fs with
-    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
-    | cons f fs' ⇒
-       ! locals ←
-         mfold_left2 ???
-          (λlocals,dst,v. reg_store dst v locals) (OK ? (locals f)) dst v;
-        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f) (carry f)) fs' m〉
-    ]
-].
-
-axiom WrongReturnValueType: String.
-
-definition is_final : state → option ((*CSC: why not res*) int) ≝
-λs. match s with
-[ State _ _ _ ⇒ None ?
-| Callstate _ _ _ _ _ ⇒ None ?
-| Returnstate v _ fs _ ⇒
-    match fs with
-     [ nil ⇒ Some ? (smerge2 v)
-     | _ ⇒ None ? ]].
-(*
-definition RTL_exec : execstep io_out io_in ≝
-  mk_execstep … ? is_final mem_of_state eval_statement.
-*)
-(* CSC: XXX the program type does not fit with the globalenv and init_mem
-definition make_initial_state : rtl_program → res (genv × state) ≝
-λp.
-  do ge ← globalenv Genv ?? p;
-  do m ← init_mem Genv ?? p;
-  let main ≝ rtl_pr_main ?? p in
-  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
-  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
-  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
-
-definition RTL_fullexec : fullexec io_out io_in ≝
-  mk_fullexec … RTL_exec ? make_initial_state.
-*)
-*)