Changeset 2909 for extracted/compiler.ml


Ignore:
Timestamp:
Mar 19, 2013, 10:21:08 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.ml

    r2905 r2909  
    601601
    602602(** val lift_cost_map_back_to_front :
    603     Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
    604     CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
     603    Csyntax.clight_program -> ASM.labelled_object_code ->
    605604    StructuredTraces.as_cost_map -> Label.clight_cost_map **)
    606 let lift_cost_map_back_to_front clight code_memory lbls k asm_cost_map =
     605let lift_cost_map_back_to_front clight oc k asm_cost_map =
    607606  StructuredTraces.lift_sigma_map_id Nat.O
    608607    (BitVectorTrie.strong_decidable_in_codomain
    609608      (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S
    610609      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    611       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (Obj.magic lbls))
    612     (Obj.magic k) (Obj.magic asm_cost_map)
     610      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
     611      (Obj.magic oc.ASM.costlabels)) (Obj.magic k) (Obj.magic asm_cost_map)
    613612
    614613open UtilBranch
     
    777776        Monad.m_bind0 (Monad.max_def Errors.res0)
    778777          (Obj.magic (assembler observe p1)) (fun p2 ->
    779 prerr_endline "COMPUTE_COST_MAP";
    780778          let k = ASMCostsSplit.aSM_cost_map p2 in
    781 prerr_endline "LIFT_COST_MAP";
    782           let k' =
    783             lift_cost_map_back_to_front p' (Fetch.load_code_memory p2.ASM.oc)
    784               p2.ASM.costlabels k
    785           in
    786 prerr_endline "END";
     779          let k' = lift_cost_map_back_to_front p' p2 k in
    787780          Monad.m_return0 (Monad.max_def Errors.res0)
    788781            { c_labelled_object_code = p2; c_stack_cost = stack_cost;
Note: See TracChangeset for help on using the changeset viewer.