Ignore:
Timestamp:
Apr 6, 2013, 7:35:25 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/extracted/fetch.ml

    r3080 r3106  
    11open Preamble
    22
     3open Types
     4
     5open Hints_declaration
     6
     7open Core_notation
     8
     9open Pts
     10
     11open Logic
     12
     13open Jmeq
     14
     15open Russell
     16
    317open Exp
    418
     
    1529open Div_and_mod
    1630
    17 open Jmeq
    18 
    19 open Russell
    20 
    21 open Types
    22 
    2331open List
    2432
     
    2937open Bool
    3038
    31 open Hints_declaration
    32 
    33 open Core_notation
    34 
    35 open Pts
    36 
    37 open Logic
    38 
    3939open Relations
    4040
     
    7979open ASM
    8080
    81 (** val inefficient_address_of_word_labels_code_mem :
    82     ASM.labelled_instruction List.list -> ASM.identifier ->
    83     BitVector.bitVector **)
    84 let inefficient_address_of_word_labels_code_mem code_mem id =
    85   Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    86     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    87     Nat.O))))))))))))))))
    88     (LabelledObjects.index_of
    89       (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag
    90         id) code_mem)
     81(** val inefficient_address_of_label :
     82    ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat **)
     83let inefficient_address_of_label instr_list id =
     84  LabelledObjects.index_of
     85    (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag id)
     86    instr_list
    9187
    9288type label_map = Nat.nat Identifiers.identifier_map
    9389
    9490(** val create_label_cost_map0 :
    95     ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
    96     BitVectorTrie.bitVectorTrie) Types.prod Types.sig0 **)
     91    ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
     92    Types.prod Types.sig0 **)
    9793let create_label_cost_map0 program =
    9894  (Types.pi1
    9995    (FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc ->
    100       (let { Types.fst = eta28695; Types.snd = ppc } =
     96      (let { Types.fst = eta19; Types.snd = ppc } =
    10197         Types.pi1 labels_costs_ppc
    10298       in
    10399      (fun _ ->
    104       (let { Types.fst = labels; Types.snd = costs } = eta28695 in
     100      (let { Types.fst = labels; Types.snd = costs } = eta19 in
    105101      (fun _ ->
    106102      (let { Types.fst = label; Types.snd = instr } = x in
     
    135131
    136132(** val create_label_cost_map :
    137     ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
    138     BitVectorTrie.bitVectorTrie) Types.prod **)
     133    ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
     134    Types.prod **)
    139135let create_label_cost_map program =
    140136  Types.pi1 (create_label_cost_map0 program)
     
    142138(** val address_of_word_labels :
    143139    ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word **)
    144 let address_of_word_labels code_mem id =
    145   let labels = (create_label_cost_map code_mem).Types.fst in
     140let address_of_word_labels program id =
     141  let labels = (create_label_cost_map program).Types.fst in
     142  let address_of_label = fun l ->
     143    Identifiers.lookup_def PreIdentifiers.ASMTag labels l Nat.O
     144  in
    146145  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    147146    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    148     Nat.O))))))))))))))))
    149     (Identifiers.lookup_def PreIdentifiers.ASMTag labels id Nat.O)
    150 
    151 (** val bitvector_max_nat : Nat.nat -> Nat.nat **)
    152 let bitvector_max_nat length =
    153   Exp.exp (Nat.S (Nat.S Nat.O)) length
    154 
    155 (** val code_memory_size : Nat.nat **)
    156 let code_memory_size =
    157   bitvector_max_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    158     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    159     Nat.O))))))))))))))))
     147    Nat.O)))))))))))))))) (address_of_label id)
    160148
    161149(** val prod_inv_rect_Type0 :
Note: See TracChangeset for help on using the changeset viewer.