Changeset 3259 for src/joint


Ignore:
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:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/StatusSimulationUtils.ma

    r3154 r3259  
    419419  ∀n.stack_sizes f1 = return n → 
    420420  ∀st1'.
    421   setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' →
     421  setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … n (joint_if_params … fn1)
     422   arg f1 st1_pre = return st1' →
    422423  st_rel st1 st2 → 
    423424  ∀t_fn1.
     
    444445         (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧
    445446       ∃st2_after_call.
    446          setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre
     447         setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) … n
     448          (joint_if_params … t_fn1) arg' f1 st2_pre
    447449          = return st2_after_call ∧
    448450       bind_new_P' ??
     
    515517   ∀ssize_f1.stack_sizes f1 = return ssize_f1 →   
    516518   ∀st1'.
    517     setup_call ?? P_in ssize_f1 (joint_if_params … fn1) arg
     519    setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … ssize_f1
     520     (joint_if_params … fn1) arg f1
    518521     (decrement_stack_usage P_in ssize_f (st_no_pc … st1)) = return st1' →
    519522   st_rel st1 st2 → 
     
    533536         st2_pre_call = return bl ∧
    534537       ∃st2_after.
    535         setup_call ?? P_out ssize_f1 (joint_if_params … t_fn1) arg'
     538        setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) …
     539         ssize_f1 (joint_if_params … t_fn1) arg' f1
    536540         (decrement_stack_usage P_out ssize_f st2_pre_call) = return st2_after ∧
    537541       bind_new_P' ??
  • src/joint/joint_semantics.ma

    r3154 r3259  
    221221   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    222222     type of arguments. To be fixed using a dependent type *)
    223   ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
     223  ; setup_call : ∀globals.∀ge : genv_gen F globals.nat → paramsT … uns_pars → call_args uns_pars → ident →
    224224      state st_pars → res (state st_pars)
    225225  ; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
     
    585585λst : state p.
    586586! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    587 ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
     587! st' ← setup_call … ge … stack_size (joint_if_params … globals fn) args i st ;
    588588return increment_stack_usage … stack_size st'.
    589589
Note: See TracChangeset for help on using the changeset viewer.