Changeset 3083 for src


Ignore:
Timestamp:
Apr 4, 2013, 9:58:03 AM (7 years ago)
Author:
sacerdot
Message:

The cost and stack* variables are now initialized with the cost of
the pre-main and the size of globals.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r3022 r3083  
    8787definition back_end :
    8888 observe_pass → costlabel → RTLabs_program →
    89   res (pseudo_assembly_program × stack_cost_model × nat) ≝
     89  res (pseudo_assembly_program × costlabel × stack_cost_model × nat) ≝
    9090λobserve,init_cost,p.
    9191  let p ≝ rtlabs_to_rtl init_cost p in
     
    105105  let i ≝ observe lin_pass 〈p,st〉 in
    106106   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
    107    return 〈p,stack_cost,max_stack〉.
     107   return 〈〈p,init_cost〉,stack_cost,max_stack〉.
    108108
    109109(* The assembler *)
     
    148148 ; c_stack_cost: stack_cost_model
    149149 ; c_max_stack: nat
     150 ; c_init_costlabel: costlabel
    150151 ; c_labelled_clight: clight_program
    151152 ; c_clight_cost_map: clight_cost_map
     
    155156λobserve,p.
    156157  ! 〈init_cost,p',p〉 ← front_end observe p;
    157   ! 〈p,stack_cost,max_stack〉 ← back_end observe init_cost p;
     158  ! 〈p_init_costlabel,stack_cost,max_stack〉 ← back_end observe init_cost p;
     159  let 〈p,init_costlabel〉 ≝ p_init_costlabel in
    158160  ! p ← assembler observe p;
    159161  let k ≝ ASM_cost_map p in
    160162  let k' ≝
    161163   lift_cost_map_back_to_front p k in
    162   return mk_compiler_output p stack_cost max_stack p' k'.
     164  return mk_compiler_output p stack_cost max_stack init_costlabel p' k'.
Note: See TracChangeset for help on using the changeset viewer.