Changeset 2796 for src/joint

Timestamp:

Mar 7, 2013, 12:10:42 PM (8 years ago)

Author:

tranquil

Message:

• added global notation for existence in Type[1] (\exists[1] x.P)
• in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
• in joint_semantics, moved out and around some parameters in primitive semantics functions
• fixed all back end semantics
• added skeleton files for single passes correctness proofs

Location:

src/joint

Files:

• Traces.ma (modified) (1 diff)
• joint_semantics.ma (modified) (9 diffs)
• semanticsUtils.ma (modified) (2 diffs)

src/joint/Traces.ma

@@ -291 +291 @@
    (* as_call_ident ≝ *) (joint_call_ident p)
    (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
+
+(* alternative definition with integrated prog_params constructor *)
+definition joint_status :
+ ∀p : sem_params.
+ joint_program p → (ident → option ℕ) → abstract_status ≝
+λp,prog,stacksizes.joint_abstract_status (mk_prog_params p prog stacksizes).

src/joint/joint_semantics.ma

@@ -199 +199 @@
       state st_pars → res (list beval)
   ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
-    ident → F globals (* current *) → state st_pars → res (state st_pars)
+    ident (* current *) → state st_pars → res (state st_pars)
   ; pop_frame: ∀globals.∀ge : genv_gen F globals.
-    ident → F globals (* current *) → state st_pars → res (state st_pars × program_counter)
+    ident (* current *) → call_dest uns_pars (* current ret *) →
+      state st_pars → res (state st_pars × program_counter)
   }.
 
@@ -407 +408 @@
 definition eval_seq_no_pc :
  ∀p:sem_params.∀globals.∀ge:genv p globals.ident →
- joint_closed_internal_function p globals →
   joint_seq p globals → state p →
   res (state p) ≝
- λp,globals,ge,curr_id,curr_fn,seq,st.
+ λp,globals,ge,curr_id,seq,st.
  match seq with
   [ extension_seq c ⇒
-    eval_ext_seq … ge c curr_id curr_fn st
+    eval_ext_seq … ge c curr_id st
   | LOAD dst addrl addrh ⇒
     ! vaddrh ← dph_arg_retrieve … st addrh ;
@@ -539 +539 @@
 definition eval_statement_no_pc :
  ∀p:sem_params.∀globals.∀ge:genv p globals.
- ident → joint_closed_internal_function p globals (* current *) →
+ ident (* current *) →
  joint_statement p globals → state p → res (state p) ≝
- λp,globals,ge,curr_id,curr_fn,s,st.
+ λp,globals,ge,curr_id,s,st.
   match s with
   [ sequential s next ⇒
     match s with
-    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id curr_fn s st 
+    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id s st 
     | _ ⇒ return st
     ]
@@ -553 +553 @@
 definition eval_return ≝
 λp : sem_params.λglobals : list ident.λge : genv p globals.
-λcurr_id.λcurr_fn : joint_closed_internal_function ??.
+λcurr_id.λcurr_ret : call_dest p.
 λst : state p.
-! st' ← pop_frame … ge curr_id curr_fn st ;
+! st' ← pop_frame … ge curr_id curr_ret st ;
 ! nxt ← next_of_call_pc … ge (\snd … st') ;
 return
@@ -562 +562 @@
 definition eval_tailcall ≝
 λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f.
-λcurr_fn : joint_closed_internal_function ??.
+λcurr_ret : call_dest p.
 λst : state_pc p.
 ! bl ← block_of_call … ge f st : IO ???;
@@ -572 +572 @@
   return mk_state_pc … st' pc (last_pop … st)
 | External efd ⇒
-  let curr_dest ≝ joint_if_result ?? curr_fn in
-  ! st' ← eval_external_call … efd args curr_dest st ;
-  eval_return … ge curr_f curr_fn st
+  ! st' ← eval_external_call … efd args curr_ret st ;
+  eval_return … ge curr_f curr_ret st
 ].
 
@@ -598 +597 @@
     ]
   | final s ⇒
+    let curr_ret ≝ joint_if_result … curr_fn in
     match s with
     [ GOTO l ⇒ goto … ge l st
-    | RETURN ⇒ eval_return … ge curr_id curr_fn st
+    | RETURN ⇒ eval_return … ge curr_id curr_ret st
     | TAILCALL _ f args ⇒
-      eval_tailcall … ge f args curr_id curr_fn st
+      eval_tailcall … ge f args curr_id curr_ret st
     ]
   | FCOND _ a lbltrue lblfalse ⇒
@@ -618 +618 @@
   λp,globals,ge,st.
   ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
-  ! st' ← eval_statement_no_pc … ge id fn s st : IO ???;
+  ! st' ← eval_statement_no_pc … ge id s st : IO ???;
   let st'' ≝ set_no_pc … st' st in
   eval_statement_advance … ge id fn s st''.
 
-(* Paolo: what if in an intermediate language main finishes with an external
-  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
-  not static... *)
 definition is_final: ∀p: sem_params.∀globals.
   genv p globals → program_counter → state_pc p → option int ≝
@@ -632 +629 @@
   [ final s' ⇒
     match s' with
-    [ RETURN ⇒ 
-      do st' ← pop_frame … ge id fn st;
+    [ RETURN ⇒
+      let curr_ret ≝ joint_if_result … fn in
+      do st' ← pop_frame … ge id curr_ret st;
       if eq_program_counter (\snd … st') exit then 
-      do vals ← read_result … ge (joint_if_result … fn) st ;
+      do vals ← read_result … ge curr_ret st ;
         Word_of_list_beval vals
       else

src/joint/semanticsUtils.ma

@@ -50 +50 @@
 }.
 
-definition reg_store ≝ λreg,v,locals. OK ? (add RegisterTag beval locals reg v).
+definition reg_store ≝ λreg,v,locals.add RegisterTag beval locals reg v.
 
 definition reg_retrieve : register_env beval → register → res beval ≝
@@ -56 +56 @@
 
 definition reg_sp_store ≝ λreg,v,locals.
-! locals' ← reg_store reg v (reg_sp_env locals) ;
-return mk_reg_sp locals' (stackp locals).
-
-definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
-
+let locals' ≝ reg_store reg v (reg_sp_env locals) in
+mk_reg_sp locals' (stackp locals).
+
+unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
+
+definition reg_sp_retrieve ≝ λlocals : reg_sp.reg_retrieve locals.
+
+definition reg_sp_init ≝ mk_reg_sp (empty_map …).
 (*** Store/retrieve on hardware registers ***)