Changeset 2774


Ignore:
Timestamp:
Mar 5, 2013, 6:15:06 PM (7 years ago)
Author:
sacerdot
Message:
  1. the compiler now outputs both the stack cost model and the max stack available
  2. hypothesis on initial status not failing removed from correctness.ma by using the low level definition
Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2739 r2774  
    443443qed.
    444444
     445definition first_free_stack_addr : ltl_program → nat ≝
     446 λp.
     447  let globals_addr_internal ≝
     448   λoffset : nat.
     449   λx_size: ident × region × nat.
     450    let 〈x, region, size〉 ≝ x_size in
     451     offset + size in
     452 foldl … globals_addr_internal 0 (prog_vars … p).
     453
    445454definition ertlptr_to_ltl:
    446  fixpoint_computer → coloured_graph_computer → ertlptr_program → ltl_program ≝
    447   λthe_fixpoint,build.
    448    b_graph_transform_program … (translate_data the_fixpoint build).
     455 fixpoint_computer → coloured_graph_computer → ertlptr_program →
     456  ltl_program × stack_cost_model × nat ≝
     457  λthe_fixpoint,build,pr.
     458   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
     459   〈ltlprog, stack_cost … ltlprog, 2^16 - first_free_stack_addr ltlprog〉.
  • src/RTLabs/RTLabsToRTL.ma

    r2689 r2774  
    11include "RTLabs/RTLabs_syntax.ma".
    22include "RTL/RTL.ma".
    3 include "common/AssocList.ma".
    43include "common/FrontEndOps.ma".
    54include "common/Graphs.ma".
  • src/compiler.ma

    r2767 r2774  
    3232axiom colour_graph : coloured_graph_computer.
    3333
    34 definition back_end : RTLabs_program → res pseudo_assembly_program ≝
     34definition back_end :
     35 RTLabs_program →
     36  res (pseudo_assembly_program × stack_cost_model × nat) ≝
    3537λp.
    3638  let p ≝ rtlabs_to_rtl p in
    3739  let p ≝ rtl_to_ertl p in
    3840  let p ≝ ertl_to_ertlptr p in
    39   let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
     41  let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
    4042  let p ≝ ltl_to_lin p in
    41           opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p).
     43  let p ≝ lin_to_asm p in
     44   match p with
     45   [ None ⇒ Error … (msg AssemblyTooLarge)
     46   | Some p ⇒ OK … 〈p,stack_cost,max_stack〉 ].
    4247
    4348include "ASM/Policy.ma".
     
    7176include "ASM/ASMCostsSplit.ma".
    7277
    73 definition compile : clight_program →
    74   res (labelled_object_code × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
     78record compiler_output : Type[0] ≝
     79 { c_labelled_object_code: labelled_object_code
     80 ; c_stack_cost: stack_cost_model
     81 ; c_max_stack: nat
     82 ; c_labelled_clight: clight_program
     83 ; c_clight_cost_map: clight_cost_map c_labelled_clight
     84 }.
     85
     86definition compile : clight_program → res compiler_output ≝
    7587λp.
    7688  ! 〈init_cost,p',p〉 ← front_end p;
    77   ! p ← back_end p;
     89  ! 〈p,stack_cost,max_stack〉 ← back_end p;
    7890  ! p ← assembler p;
    7991  let k ≝ ASM_cost_map p in
    8092  let k' ≝
    8193   lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in
    82   return 〈p, ❬p', k'❭〉.
     94  return mk_compiler_output p stack_cost max_stack p' k'.
  • src/correctness.ma

    r2766 r2774  
    77
    88theorem correct :
    9   ∀input_program
    10   ∀lobject_code,labelled,cost_map.
    11   compile input_program = OK ? 〈lobject_code,❬labelled,cost_map❭〉
     9  ∀input_program,output.
     10(*  ∀lobject_code,labelled,cost_map. *)
     11  compile input_program = OK ? output
    1212
    1313  not_wrong … (exec_inf … clight_fullexec input_program) →
    1414 
    15   sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
     15  sim_with_labels
     16   (exec_inf … clight_fullexec input_program)
     17   (exec_inf … clight_fullexec (c_labelled_clight … output))
    1618  ∧
    1719  True (* TODO *).
    1820
    19 #input_program
    20 #object_code #labelled #cost_map
     21#input_program #output
    2122#COMPILE
    2223#NOT_WRONG
     
    3738include "Clight/Clight_abstract.ma".
    3839include "common/Measurable.ma".
    39 
    40 (* We could restrict this function to identifiers that are function names in the
    41    program and lift it (like the lift_cost_map_back_to_front function), but
    42    let's go with the easier notion of having a total map and ignore all the
    43    extra stuff. *)
    44 definition stack_cost_T ≝ ident → nat.
    4540
    4641definition Clight_stack_ident :
     
    117112qed.
    118113
     114include "common/AssocList.ma".
     115
     116definition lookup_stack_cost : stack_cost_model → ident → nat ≝
     117 λstack_cost,id.
     118  match assoc_list_lookup ?? id (eq_identifier …) stack_cost with
     119  [ None ⇒ 0 | Some n ⇒ n ].
     120
    119121definition simulates ≝
    120   λstack_cost : stack_cost_T.  λ stack_bound, labelled, object_code, cost_map, initial_status.
    121   return initial_status = make_initial_state ?? (OC_preclassified_system object_code) it →
    122   ∀m1,m2. measurable Clight_pcs labelled m1 m2 stack_cost stack_bound →
    123   ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 →
    124   ∃n1,n2. observables Clight_pcs labelled m1 m2 = observables (OC_preclassified_system object_code) it n1 n2 ∧
     122  λp: compiler_output.
     123  let initial_status ≝ initialise_status … (load_code_memory (oc (c_labelled_object_code … p))) in
     124  ∀m1,m2.
     125   measurable Clight_pcs (c_labelled_clight … p) m1 m2
     126    (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
     127  ∀c1,c2.
     128   clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = Some ? c1 →
     129   clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = Some ? c2 →
     130  ∃n1,n2.
     131   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
     132   observables (OC_preclassified_system (c_labelled_object_code … p)) it n1 n2
     133  ∧
    125134   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
    126135
    127136theorem correct' :
    128   ∀input_program. 
    129   ∀lobject_code,labelled,cost_map,stack_cost,stack_bound,initial_status.
    130   compile input_program = OK ? 〈lobject_code,❬labelled,cost_map❭〉 →
    131 
     137  ∀input_program,output.
     138  ∀initial_status.
     139  compile input_program = OK ? output →
    132140  not_wrong … (exec_inf … clight_fullexec input_program) →
    133  
    134   return initial_status = make_initial_state ?? (OC_preclassified_system lobject_code) it →
    135  
    136   sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
     141  sim_with_labels
     142   (exec_inf … clight_fullexec input_program)
     143   (exec_inf … clight_fullexec (c_labelled_clight … output))
    137144  ∧
    138   simulates stack_cost stack_bound labelled lobject_code cost_map initial_status.
    139  
    140 
     145  simulates output.
    141146 
    142147(* start of old simulates 
  • src/joint/Joint.ma

    r2712 r2774  
    530530definition joint_program ≝
    531531 λp:params. program (joint_function p) nat.
     532
     533(* The cost model for stack consumption *)
     534definition stack_cost_model ≝ list (ident × nat).
     535
     536definition stack_cost : ∀p:params. joint_program p → stack_cost_model ≝
     537 λp,pr.
     538  foldr …
     539   (λid_fun,acc. let 〈id,fun〉 ≝ id_fun in
     540     match fun with
     541     [ Internal jif ⇒ 〈id,joint_if_stacksize ?? (pi1 … jif)〉::acc
     542     | External _ ⇒ acc ])
     543   [ ] (prog_funct ?? pr).
     544
Note: See TracChangeset for help on using the changeset viewer.