Changeset 3259 for src/joint

Timestamp:

May 9, 2013, 12:49:38 AM (8 years ago)

Author:

piccolo

Message:

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

Location:

src/joint

Files:

• StatusSimulationUtils.ma (modified) (4 diffs)
• joint_semantics.ma (modified) (2 diffs)

src/joint/StatusSimulationUtils.ma

@@ -419 +419 @@
   ∀n.stack_sizes f1 = return n →  
   ∀st1'.
-  setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' → 
+  setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … n (joint_if_params … fn1) 
+   arg f1 st1_pre = return st1' → 
   st_rel st1 st2 →  
   ∀t_fn1.
@@ -444 +445 @@
          (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧
        ∃st2_after_call.
-         setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre 
+         setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) … n 
+          (joint_if_params … t_fn1) arg' f1 st2_pre 
           = return st2_after_call ∧
        bind_new_P' ??
@@ -515 +517 @@
    ∀ssize_f1.stack_sizes f1 = return ssize_f1 →   
    ∀st1'.
-    setup_call ?? P_in ssize_f1 (joint_if_params … fn1) arg 
+    setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … ssize_f1 
+     (joint_if_params … fn1) arg f1
      (decrement_stack_usage P_in ssize_f (st_no_pc … st1)) = return st1' → 
    st_rel st1 st2 →  
@@ -533 +536 @@
          st2_pre_call = return bl ∧
        ∃st2_after.
-        setup_call ?? P_out ssize_f1 (joint_if_params … t_fn1) arg' 
+        setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) … 
+         ssize_f1 (joint_if_params … t_fn1) arg' f1
          (decrement_stack_usage P_out ssize_f st2_pre_call) = return st2_after ∧
        bind_new_P' ??

src/joint/joint_semantics.ma

@@ -221 +221 @@
    (*CSC: setup_call returns a res only because we can call a function with the wrong number and
      type of arguments. To be fixed using a dependent type *)
-  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
+  ; setup_call : ∀globals.∀ge : genv_gen F globals.nat → paramsT … uns_pars → call_args uns_pars → ident → 
       state st_pars → res (state st_pars)
   ; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
@@ -585 +585 @@
 λst : state p.
 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
-! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
+! st' ← setup_call … ge … stack_size (joint_if_params … globals fn) args i st ;
 return increment_stack_usage … stack_size st'.