Changeset 2422

Timestamp:

Oct 30, 2012, 4:23:09 PM (8 years ago)

Author:

tranquil

Message:

adapted joint to cl_call f

Location:

src/joint

Files:

• Joint.ma (modified) (5 diffs)
• SemanticUtils.ma (modified) (2 diffs)
• Traces.ma (modified) (3 diffs)
• blocks.ma (modified) (1 diff)
• linearise.ma (modified) (3 diffs)
• semantics.ma (modified) (12 diffs)
• semantics_blocks.ma (modified) (1 diff)

src/joint/Joint.ma

@@ -7 +7 @@
 include "common/LabelledObjects.ma".
 include "ASM/Util.ma".
-include "common/StructuredTraces.ma".
 
 (* Here is the structure of parameter records (downward edges are coercions,
@@ -169 +168 @@
 λp,g,P,inst. All … P (step_labels … inst).
 
-definition step_classifier :
-  ∀p.∀globals.
-    joint_step p globals → status_class ≝ λp,g,s.
-  match s with
-  [ step_seq s ⇒
-    match s with
-    [ CALL_ID _ _ _ ⇒ cl_call
-    | extension_call _ ⇒ cl_call
-    | _ ⇒ cl_other
-    ]
-  | COND _ _ ⇒ cl_jump
-  ].
-
 record stmt_params : Type[1] ≝
   { uns_pars :> unserialized_params
@@ -207 +193 @@
     ].
 
-definition fin_step_classifier :
-  ∀p : stmt_params.
-    joint_fin_step p → status_class
-  ≝ λp,s.
-  match s with
-  [ GOTO _ ⇒ cl_other
-  | _ ⇒ cl_return
-  ].
-
 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
   | sequential: joint_step p globals → succ p → joint_statement p globals
   | final: joint_fin_step p → joint_statement p globals.
-
-definition stmt_classifier :
-  ∀p : stmt_params.∀globals.
-    joint_statement p globals → status_class
-  ≝ λp,g,s.
-  match s with
-  [ sequential stp _ ⇒ step_classifier p g stp
-  | final stp ⇒ fin_step_classifier p stp
-  ].
 
 coercion extension_fin_to_fin_step : ∀p : stmt_params.
@@ -466 +434 @@
 definition joint_closed_internal_function ≝
   λp,globals.
-    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
+    Σdef : joint_internal_function p globals. code_closed … (joint_if_code … def).
 
 definition set_joint_code ≝
@@ -534 +502 @@
     (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
 
-definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
+definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
 
 definition joint_program ≝

src/joint/SemanticUtils.ma

@@ -151 +151 @@
 definition make_sem_graph_params :
   ∀pars : graph_params.
-  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
+  ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars).
   sem_params ≝
   λpars,g_pars.
@@ -190 +190 @@
 definition make_sem_lin_params :
   ∀pars : lin_params.
-  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
+  ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars).
   sem_params ≝
   λpars,g_pars.

src/joint/Traces.ma

@@ -1 +1 @@
 include "joint/semantics.ma".
+include "common/StructuredTraces.ma".
 
 record evaluation_params : Type[1] ≝
@@ -7 +8 @@
  ; ev_genv: genv sparams globals
  ; io_env : state sparams → ∀o:io_out.res (io_in o)
- } .
+ }.
+ 
+record prog_params : Type[1] ≝
+ { prog_spars : sem_params
+ ; prog : joint_program prog_spars
+ ; prog_io : state prog_spars → ∀o.res (io_in o)
+ }.
 
-(*record classifier_params : Type[1] ≝
-  { cl_pars :> evaluation_parameters
-  ; cl_ext_step : ext_step cl_pars → status_class
-  ; cl_ext_fin_stmt : ext_fin_stmt cl_pars → status_class
-  }.*)
+definition make_global : prog_params → evaluation_params
+≝
+λpars.
+(* Invariant: a -1 block is unused in common/Globalenvs *)
+let b ≝ mk_block Code (-1) in
+let ptr ≝ mk_pointer b (mk_offset (bv_zero …)) in
+let p ≝ prog pars in
+mk_evaluation_params
+  (prog_var_names … p)
+  (prog_spars pars)
+  «ptr, refl …»
+  (mk_genv_gen ?? (globalenv_noinit ? p) ?)
+  (prog_io pars).
+(* TODO or TOBEFOUND *)
+cases daemon
+qed.
 
+coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
+≝ make_global on _p : prog_params to evaluation_params.
+
+
+axiom ExternalMain : String.
+check save_frame
+
+definition make_initial_state :
+ ∀pars: prog_params.res (state_pc pars) ≝
+λpars.let p ≝ prog pars in
+  let sem_globals : evaluation_params ≝ pars in
+  let ge ≝ ev_genv sem_globals in
+  let m ≝ alloc_mem … p in
+  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
+  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
+  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in
+  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
+  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in
+  let main ≝ prog_main … p in
+  let st0 ≝ mk_state pars (empty_framesT …) spp ispp (BBbit false) (empty_regsT … spp) m in
+  (* use exit sem_globals as ra and call_dest_for_main as dest *)
+  ! st0' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
+  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
+  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
+  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ; 
+  match main_fd with
+  [ Internal fn ⇒
+    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
+  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
+  ].
+  [ %
+  | cases ispb
+  | cases spb
+  ] normalize //
+qed.
+
+definition step_flow_classifier :
+  ∀p : evaluation_params.∀F,flows.
+  step_flow p F flows → status_class ≝
+  λp,F,flows,flow.match flow with
+  [ Redirect _ _ ⇒ cl_jump
+  | Init bl _ _ _ ⇒
+    match symbol_for_block … (ev_genv p) (mk_block Code bl) with
+    [ Some f ⇒ cl_call f
+    | None ⇒ cl_other (* we don't care, as call will fail anyway *)
+    ]
+  | Proceed flows ⇒
+    match flows with
+    [ Labels lbls ⇒
+      match lbls with
+      [ nil ⇒ cl_other
+      | _ ⇒ cl_jump
+      ]
+    | _ ⇒ cl_other
+    ]
+  ].
+
+definition fin_step_flow_classifier :
+  ∀p : evaluation_params.∀F,flows.
+  fin_step_flow p F flows → status_class ≝
+  λp,F,flows,flow.match flow with
+  [ FRedirect lbls _ ⇒
+    match lbls with
+    [ nil ⇒ (* not really possible, we don't care *) cl_other
+    | cons _ tl ⇒
+      match tl with
+      [ nil ⇒ (* only one label *) cl_other
+      | _ ⇒ (* fork *) cl_jump
+      ]
+    ]
+  | FTailInit bl _ _ ⇒ (* not implemented for now, probably needs new class *)
+    cl_other
+  | _ ⇒ cl_return
+  ].
 
 definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
@@ -58 +150 @@
    (* as_pc_of ≝ *) (pc …)
    (* as_classifier ≝ *)
-    (λs,cl.∃fn,stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉 ∧
-     stmt_classifier … stmt = cl)
+    (λs,cl.∃fn,stmt.
+      fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉 ∧
+      match stmt with
+      [ sequential stp nxt ⇒
+        ∃flow,s'.
+        io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) = return 〈flow, s'〉 ∧
+        step_flow_classifier … flow = cl
+      | final stp ⇒
+        ∃flow.io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) = return flow ∧
+        fin_step_flow_classifier … flow = cl
+      ])
    (* as_label_of_pc ≝ *)
     (λpc.

src/joint/blocks.ma

@@ -239 +239 @@
 definition seq_block_step_in_code ≝
   λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst.
-  src ~❨\fst B, \fst l❩~> \snd l in c ∧ step_in_code … c (\snd l) (\snd B) dst.
+  ∃hd,tl.l = hd @ [tl] ∧
+  src ~❨\fst B, l❩~> tl in c ∧ step_in_code … c tl (\snd B) dst.
 
 definition seq_block_fin_step_in_code ≝
   λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit.
-  src ~❨\fst B, \fst l❩~> \snd l in c ∧ fin_step_in_code … c (\snd l) (\snd B).
+  ∃hd,tl.l = hd @ [tl] ∧
+  src ~❨\fst B, l❩~> tl in c ∧ fin_step_in_code … c tl (\snd B).
 
 (* generates ambiguity even if it shouldn't

src/joint/linearise.ma

@@ -652 +652 @@
   ∀p : unserialized_params.
   ∀globals.
-    joint_internal_function (mk_graph_params p) globals →
-    joint_internal_function (mk_lin_params p) globals
+    joint_closed_internal_function (mk_graph_params p) globals →
+    joint_closed_internal_function (mk_lin_params p) globals
      (* ∃sigma : identifier_map LabelTag ℕ. 
         let g ≝ joint_if_code ?? (pi1 … fin) in
@@ -669 +669 @@
                     (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
                     (stmt_implicit_label … s)) (nth_opt … n c)*) ≝
-  λp,globals,f_in.
-  mk_joint_internal_function (mk_lin_params p) globals
+  λp,globals,f_sig.let f_in ≝ pi1 … f_sig in
+  «mk_joint_internal_function (mk_lin_params p) globals
    (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in)
    (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in)
    (joint_if_stacksize ?? f_in)
-   (linearise_code p globals (joint_if_code … f_in)
-   (match daemon in False with [ ])
-   (joint_if_entry … f_in))
-   0 0 (* exit is dummy! *).
+   (linearise_code p globals (joint_if_code … f_in) (pi2 … f_sig) (joint_if_entry … f_in))
+   0 0 (* exit is dummy! *), ?».
 elim (linearise_code ?????) #c * #code_closed
+[3: #_ assumption ]
 @hide_prf
 * #sigma * #O_in #sigma_prop
@@ -688 +687 @@
 ]
 qed.
+
+definition linearise : ∀p : unserialized_params.
+  program (joint_function (mk_graph_params p)) ℕ →
+  program (joint_function (mk_lin_params p)) ℕ ≝
+  λp,pr.transform_program ??? pr
+    (λglobals.transf_fundef ?? (linearise_int_fun p globals)).

src/joint/semantics.ma

@@ -17 +17 @@
 }.
 
-definition genv ≝ λp.genv_gen (joint_internal_function p).
+definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
 coercion genv_to_genv_t :
   ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
   λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.
-
 definition cpointer ≝ Σp.ptype p = Code.
 definition xpointer ≝ Σp.ptype p = XData.
 unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
 unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
+unification hint 0 ≔ p,g ⊢
+  joint_closed_internal_function p g ≡
+  Sig (joint_internal_function p g) (λfd.code_closed p g (joint_if_code p g fd)).
 
 record sem_state_params : Type[1] ≝
@@ -82 +84 @@
   genv pars globals →
   block →
-  res (joint_internal_function pars globals) ≝
+  res (joint_closed_internal_function pars globals) ≝
   λpars,globals,ge,b.
   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
@@ -95 +97 @@
   genv pars globals →
   cpointer →
-  res (joint_internal_function pars globals) ≝
+  res (joint_closed_internal_function pars globals) ≝
  λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
 
@@ -149 +151 @@
   ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
       F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
+  ; ext_tailcall_id : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
+      state st_pars → IO io_out io_in ident
   ; eval_ext_call: ∀globals.genv_gen F globals →
       ext_call uns_pars → state st_pars →
       IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
+  ; ext_call_id : ∀globals.genv_gen F globals → ext_call uns_pars →
+      state st_pars → IO io_out io_in ident
   ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars)
   (* do something more in some op2 calculations (e.g. mark a register for correction
@@ -266 +272 @@
 (* parameters that are defined by serialization *)
 record more_sem_params (pp : params) : Type[1] ≝
-  { msu_pars :> more_sem_unserialized_params pp (joint_internal_function pp)
+  { msu_pars :> more_sem_unserialized_params pp (joint_closed_internal_function pp)
   ; offset_of_point : code_point pp → option offset (* can overflow *)
   ; point_of_offset : offset → code_point pp
@@ -347 +353 @@
 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
   genv p globals → cpointer →
-  res ((joint_internal_function p globals) × (joint_statement p globals)) ≝
+  res ((joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
   λp,msp,globals,ge,ptr.
   let pt ≝ point_of_pointer ? msp ptr in
@@ -427 +433 @@
 
 definition eval_seq_no_pc :
- ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals →
+ ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals →
   state p → ∀s:joint_seq p globals.
   IO io_out io_in (state p) ≝
@@ -513 +519 @@
 definition eval_step :
  ∀p:sem_params.∀globals. genv p globals →
-  joint_internal_function p globals → state p →
+  joint_closed_internal_function p globals → state p →
   ∀s:joint_step p globals.
   IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
@@ -533 +539 @@
 
 definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
-  (* current function *) joint_internal_function p globals → state p → ∀s : joint_fin_step p.
+  (* current function *) joint_closed_internal_function p globals → state p → ∀s : joint_fin_step p.
   IO io_out io_in (state p) ≝
  λp,globals,ge,curr_fn,st,s.
@@ -544 +550 @@
 
 definition eval_fin_step_pc :
- ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals → state p →
+ ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals → state p →
   ∀s:joint_fin_step p.
   IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
@@ -557 +563 @@
 
 definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
-  state p → Z → joint_internal_function p globals → call_args p →
+  state p → Z → joint_closed_internal_function p globals → call_args p →
   res (state_pc p) ≝
   λp,globals,ge,st,id,fn,args.
@@ -600 +606 @@
 definition eval_statement :
  ∀globals.∀p:sem_params.genv p globals →
-  state_pc p → joint_internal_function p globals → joint_statement p globals →
+  state_pc p → joint_closed_internal_function p globals → joint_statement p globals →
     IO io_out io_in (state_pc p) ≝
  λglobals,p,ge,st,curr_fn,stmt.

src/joint/semantics_blocks.ma

@@ -232 +232 @@
   %* #H @H -H
   lapply tl_other lapply rest_in_code
-  (* BUG? cases tl causes "Ill formed pattern" *)
-  @(match tl with [ nil ⇒ ? | cons hd' tl' ⇒ ?])
+  cases tl [2: #hd' #tl' ]
   cases rest [2,4: #mid' #rest']
-  [1,4: * ]
+  [2,3: * ]
   [2: whd in ⊢ (%→?); #EQ' destruct(EQ') *
   | ** #nxt' * #at_mid #_ #_ * #mid_other #_