Changeset 1383 for src/LIN


Ignore:
Timestamp:
Oct 15, 2011, 12:13:23 AM (8 years ago)
Author:
sacerdot
Message:

Potential bug fixed and bug found: the way pointers and labels are put in
bijection must be different between LIN and graph-like languages (bug fixed).
Moreover, in both cases it must be possible to retrieve the function from the
address and the easiest (only?) way to do that is to use the block of the
address to store the block of the function, and put the offsets in bijection
with labels/offsets, preventing pointer mangling since the pointer is in
the Code region (found, to be fixed).

Location:
src/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1382 r1383  
    33
    44(*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
    5 definition ltl_lin_more_sem_params: ∀succT:Type[0].∀succ:succT → address → res address. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
    6  λsuccT,succ.
     5definition ltl_lin_more_sem_params: ∀succT,succ,pointer_of_label. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
     6 λsuccT,succ,pointer_of_label.
    77 mk_more_sem_params ?
    88  unit hw_register_env succ
     
    2222
    2323definition ltl_lin_sem_params:
    24  ∀succT:Type[0].∀succ:succT → address → res address. sem_params ≝
    25  λsuccT,succ.mk_sem_params … (ltl_lin_more_sem_params … succ).
     24 ∀succT,succ,pointer_of_label. sem_params ≝
     25 λsuccT,succ,pointer_of_label.mk_sem_params … (ltl_lin_more_sem_params succT succ pointer_of_label).
     26
    2627
    2728definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    2829definition ltl_lin_pop_frame:
    29  ∀succT:Type[0].∀succ:succT → address → res address. state … (ltl_lin_sem_params … succ) → res ((state … (ltl_lin_sem_params … succ)) × address) ≝
    30  λ_.λ_.fetch_ra ….
     30 ∀succT,succ,pointer_of_label. state … (ltl_lin_sem_params succT succ pointer_of_label) → res ((state … (ltl_lin_sem_params … succ pointer_of_label)) × address) ≝
     31 λ_.λ_.λ_.fetch_ra ….
    3132definition ltl_lin_save_frame:
    32  ∀succT:Type[0].∀succ:succT → address → res address. address → nat → unit → nat → unit → state … (ltl_lin_sem_params … succ) → res (state … (ltl_lin_sem_params … succ)) ≝
    33  λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
     33 ∀succT,succ,pointer_of_label. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
     34 λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    3435
    35 definition ltl_lin_more_sem_params1 : ∀succT:Type[0].∀succ:succT → address → res address.more_sem_params1 … ltl_lin_params1 ≝
    36  λsuccT,succ.
    37  mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params ? succ)
    38   ltl_lin_init_locals (ltl_lin_pop_frame … succ) (ltl_lin_save_frame … succ).
     36definition ltl_lin_more_sem_params1 : ∀succT,succ,pointer_of_label.more_sem_params1 … ltl_lin_params1 ≝
     37 λsuccT,succ,pointer_of_label.
     38 mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params succT succ pointer_of_label)
     39  ltl_lin_init_locals (ltl_lin_pop_frame …) (ltl_lin_save_frame …).
    3940
    4041(*CSC: XXXXX, for is_final only *)
    41 axiom ltl_lin_fetch_result: ∀succT:Type[0].∀succ:succT → address → res address.state (ltl_lin_sem_params … succ) → res (list beval).
     42axiom ltl_lin_fetch_result: ∀succT,succ,pointer_of_label.state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval).
    4243
    4344(*CSC: XXXX, for external functions only*)
    44 axiom ltl_lin_fetch_external_args: ∀succT:Type[0].∀succ:succT → address → res address.external_function → state (ltl_lin_sem_params … succ) → res (list val).
    45 axiom ltl_lin_set_result: ∀succT:Type[0].∀succ:succT → address → res address.list val → state (ltl_lin_sem_params … succ) → res (state (ltl_lin_sem_params … succ)).
     45axiom ltl_lin_fetch_external_args: ∀succT,succ,pointer_of_label.external_function → state (ltl_lin_sem_params succT succ pointer_of_label) → res (list val).
     46axiom ltl_lin_set_result: ∀succT,succ,pointer_of_label.list val → state (ltl_lin_sem_params succT succ pointer_of_label) → res (state (ltl_lin_sem_params … succ pointer_of_label)).
    4647
    47 definition ltl_lin_exec_extended: ∀succT:Type[0].∀succ:succT → address → res address.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params … succ) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ)))
    48  ≝ λsuccT,succ,p,globals,ge,abs. ⊥.
     48definition ltl_lin_exec_extended: ∀succT,succ,pointer_of_label.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT succ pointer_of_label) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ pointer_of_label)))
     49 ≝ λsuccT,succ,pointer_of_label,p,globals,ge,abs. ⊥.
    4950@abs qed.
    5051
    5152definition ltl_lin_more_sem_params2:
    52  ∀succT,succ,codeT,lookup,fetch.
     53 ∀succT,succ,pointer_of_label,codeT,lookup,fetch.
    5354 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
    54  λsuccT,succ,codeT,lookup,fetch,globals.
    55   mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ)
     55 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
     56  mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label)
    5657   (fetch globals) (ltl_lin_fetch_result …) (ltl_lin_fetch_external_args …)
    5758   (ltl_lin_set_result …) (ltl_lin_exec_extended …).
    5859
    5960definition ltl_lin_fullexec ≝
    60  λsuccT,succ,codeT,lookup,fetch.
    61   joint_fullexec … (λp. ltl_lin_more_sem_params2 succT succ codeT lookup fetch (prog_var_names … p)).
     61 λsuccT,succ,pointer_of_label,codeT,lookup,fetch.
     62  joint_fullexec … (λp. ltl_lin_more_sem_params2 succT succ pointer_of_label codeT lookup fetch (prog_var_names … p)).
  • src/LIN/semantics.ma

    r1382 r1383  
    55 λ_.λaddr. addr_add addr 1.
    66
    7 (*CSC: XXXXXXXXXX *)
    8 axiom lin_fetch_statement: ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc) → res (pre_lin_statement globals).
     7axiom lin_pointer_of_label: label → Σp:pointer. ptype p = Code.
    98
    10 definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement.
     9axiom NotFound: String.
     10axiom lin_fetch_statement:
     11 ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals).(* ≝
     12 λglobals,ge,st.
     13  let pc ≝ pc … st in
     14 ?.
     15  let fn ≝ ? in
     16  opt_to_res ? [MSG NotFound] (lookup … (lin_params …) (joint_if_code … fn) ?(*label???*)).
     17*)
     18
     19definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc lin_pointer_of_label … lin_fetch_statement.
Note: See TracChangeset for help on using the changeset viewer.