Changeset 2717 for extracted/compiler.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.ml

    r2649 r2717  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open CostLabel
    46
     
    3133open Identifiers
    3234
     35open Exp
     36
    3337open Arithmetic
    3438
     
    148152
    149153open Initialisation
    150 
    151 open BitVectorTrie
    152154
    153155open Graphs
     
    175177        init_cost; Types.snd = p' }; Types.snd = p5 }))
    176178
     179open Deqsets
     180
     181open State
     182
     183open Bind_new
     184
     185open BindLists
     186
     187open Blocks
     188
     189open TranslateUtils
     190
     191open AssocList
     192
    177193open String
    178194
    179195open LabelledObjects
    180196
     197open I8051
     198
     199open BackEndOps
     200
     201open Joint
     202
     203open RTL
     204
     205open RTLabsToRTL
     206
     207open ERTL
     208
     209open RegisterSet
     210
     211open RTLToERTL
     212
     213open ERTLptr
     214
     215open ERTLToERTLptr
     216
     217open Fixpoints
     218
     219open Set_adt
     220
     221open Liveness
     222
     223open Interference
     224
     225open Joint_LTL_LIN
     226
     227open LTL
     228
     229open ERTLptrToLTL
     230
     231open LIN
     232
     233open Linearise
     234
     235open LTLToLIN
     236
    181237open ASM
     238
     239open BitVectorTrieSet
     240
     241open LINToASM
     242
     243(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
     244let compute_fixpoint _ =
     245  failwith "AXIOM TO BE REALIZED"
     246
     247(** val colour_graph : Interference.coloured_graph_computer **)
     248let colour_graph _ =
     249  failwith "AXIOM TO BE REALIZED"
    182250
    183251(** val back_end :
    184252    RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program **)
    185 let back_end x =
    186   failwith "AXIOM TO BE REALIZED"
     253let back_end p =
     254  let p0 = RTLabsToRTL.rtlabs_to_rtl p in
     255  let p3 = RTLToERTL.rtl_to_ertl p0 in
     256  let p4 = ERTLToERTLptr.ertl_to_ertlptr p3 in
     257  let p5 = ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p4 in
     258  let p6 = LTLToLIN.ltl_to_lin p5 in LINToASM.lin_to_asm p6
    187259
    188260type object_code = BitVector.byte List.list
    189261
    190 type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
     262type costlabel_map1 = CostLabel.costlabel BitVectorTrie.bitVectorTrie
     263
     264open Assembly
     265
     266open Status
     267
     268open Fetch
     269
     270open PolicyFront
     271
     272open PolicyStep
     273
     274open Policy
    191275
    192276(** val assembler :
    193     ASM.pseudo_assembly_program -> (object_code, costlabel_map) Types.prod
     277    ASM.pseudo_assembly_program -> (object_code, costlabel_map1) Types.prod
    194278    Errors.res **)
    195 let assembler x =
    196   failwith "AXIOM TO BE REALIZED"
     279let assembler p =
     280  let { Types.fst = preamble0; Types.snd = list_instr } = p in
     281  let p' = { Types.fst = preamble0; Types.snd = list_instr } in
     282  Obj.magic
     283    (Monad.m_bind0 (Monad.max_def Errors.res0)
     284      (Obj.magic
     285        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
     286          (Policy.jump_expansion' (Types.coerc_pair_sigma p'))))
     287      (fun sigma_pol ->
     288      let sigma0 = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
     289      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
     290      Obj.magic (Errors.OK (Types.pi1 (Assembly.assembly p sigma0 pol)))))
    197291
    198292open StructuredTraces
     
    200294open AbstractStatus
    201295
    202 open Status
    203 
    204296open StatusProofs
    205297
    206298open Interpret
    207 
    208 open Fetch
    209299
    210300open ASMCosts
     
    223313
    224314(** val compile :
    225     Csyntax.clight_program -> ((object_code, costlabel_map) Types.prod,
     315    Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,
    226316    (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
    227317    Errors.res **)
Note: See TracChangeset for help on using the changeset viewer.