Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (7 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.mli

    r2773 r2775  
    199199open TranslateUtils
    200200
    201 open AssocList
    202 
    203201open String
    204202
     
    256254
    257255val back_end :
    258   RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program Errors.res
     256  RTLabs_syntax.rTLabs_program -> ((ASM.pseudo_assembly_program,
     257  Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
    259258
    260259open Assembly
     
    290289open ASMCostsSplit
    291290
    292 val compile :
    293   Csyntax.clight_program -> (ASM.labelled_object_code,
    294   (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
    295   Errors.res
    296 
     291type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
     292                         c_stack_cost : Joint.stack_cost_model;
     293                         c_max_stack : Nat.nat;
     294                         c_labelled_clight : Csyntax.clight_program;
     295                         c_clight_cost_map : Label.clight_cost_map }
     296
     297val compiler_output_rect_Type4 :
     298  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
     299  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
     300  -> 'a1
     301
     302val compiler_output_rect_Type5 :
     303  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
     304  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
     305  -> 'a1
     306
     307val compiler_output_rect_Type3 :
     308  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
     309  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
     310  -> 'a1
     311
     312val compiler_output_rect_Type2 :
     313  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
     314  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
     315  -> 'a1
     316
     317val compiler_output_rect_Type1 :
     318  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
     319  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
     320  -> 'a1
     321
     322val compiler_output_rect_Type0 :
     323  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
     324  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
     325  -> 'a1
     326
     327val c_labelled_object_code : compiler_output -> ASM.labelled_object_code
     328
     329val c_stack_cost : compiler_output -> Joint.stack_cost_model
     330
     331val c_max_stack : compiler_output -> Nat.nat
     332
     333val c_labelled_clight : compiler_output -> Csyntax.clight_program
     334
     335val c_clight_cost_map : compiler_output -> Label.clight_cost_map
     336
     337val compiler_output_inv_rect_Type4 :
     338  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
     339  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
     340  'a1
     341
     342val compiler_output_inv_rect_Type3 :
     343  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
     344  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
     345  'a1
     346
     347val compiler_output_inv_rect_Type2 :
     348  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
     349  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
     350  'a1
     351
     352val compiler_output_inv_rect_Type1 :
     353  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
     354  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
     355  'a1
     356
     357val compiler_output_inv_rect_Type0 :
     358  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
     359  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
     360  'a1
     361
     362val compiler_output_discr : compiler_output -> compiler_output -> __
     363
     364val compiler_output_jmdiscr : compiler_output -> compiler_output -> __
     365
     366val compile : Csyntax.clight_program -> compiler_output Errors.res
     367
Note: See TracChangeset for help on using the changeset viewer.