Changeset 2909


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

New extraction.

Location:
extracted
Files:
10 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSMCosts.ml

    r2905 r2909  
    115115open Interpret
    116116
     117(** val aSMRegisterRets : ASM.subaddressing_mode List.list **)
     118let aSMRegisterRets =
     119  List.Cons ((ASM.DIRECT
     120    (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     121      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     122      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     123      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     124      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     125      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     126      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     127      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     128      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     129      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     130      Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
     131    (List.Cons ((ASM.DIRECT
     132    (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     133      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     134      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     135      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     136      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     137      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     138      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     139      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     140      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     141      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     142      Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
     143    (List.Cons ((ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
     144    Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
     145    (Nat.O, Bool.False, Vector.VEmpty))))))), (List.Cons ((ASM.REGISTER
     146    (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
     147    Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
     148    Vector.VEmpty))))))), List.Nil)))))))
     149
     150(** val as_result_of_finaladdr :
     151    'a1 -> 'a1 Status.preStatus -> BitVector.word -> Integers.int
     152    Types.option **)
     153let as_result_of_finaladdr cm st finaladdr =
     154  match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     155          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     156          Nat.O)))))))))))))))) st.Status.program_counter finaladdr with
     157  | Bool.True ->
     158    let vals =
     159      List.map (fun h ->
     160        Status.get_arg_8 cm st Bool.False
     161          (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
     162            Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     163            (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
     164            ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct,
     165            (Vector.VCons (Nat.O, ASM.Registr, Vector.VEmpty))))))
     166            (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     167            (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
     168            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
     169            ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     170            (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
     171            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
     172            (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
     173            ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
     174            ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
     175            ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
     176            (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
     177            (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
     178            h)) aSMRegisterRets
     179    in
     180    let dummy =
     181      BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     182        Nat.O))))))))
     183    in
     184    let first_byte = fun l ->
     185      match l with
     186      | List.Nil -> { Types.fst = dummy; Types.snd = List.Nil }
     187      | List.Cons (hd, tl) -> { Types.fst = hd; Types.snd = tl }
     188    in
     189    let { Types.fst = b1; Types.snd = tl1 } = first_byte vals in
     190    let { Types.fst = b2; Types.snd = tl2 } = first_byte tl1 in
     191    let { Types.fst = b3; Types.snd = tl3 } = first_byte tl2 in
     192    let { Types.fst = b4; Types.snd = tl4 } = first_byte tl3 in
     193    Types.Some
     194    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     195      Nat.O))))))))
     196      (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     197        Nat.O))))))))
     198        (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     199          Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     200          (Nat.S Nat.O)))))))))) b4
     201      (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     202        Nat.O))))))))
     203        (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     204          Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     205          (Nat.S Nat.O))))))))) b3
     206        (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     207          (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     208          (Nat.S (Nat.S Nat.O)))))))) b2 b1)))
     209  | Bool.False -> Types.None
     210
    117211(** val oC_abstract_status :
    118     BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    119     BitVectorTrie.bitVectorTrie -> StructuredTraces.abstract_status **)
    120 let oC_abstract_status code_memory cost_labels =
     212    ASM.labelled_object_code -> StructuredTraces.abstract_status **)
     213let oC_abstract_status prog =
     214  let code_memory = Fetch.load_code_memory prog.ASM.oc in
    121215  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
    122     StructuredTraces.as_pc_of =
    123     (Obj.magic (Status.program_counter code_memory));
    124     StructuredTraces.as_classify =
    125     (Obj.magic (AbstractStatus.oC_classify code_memory));
    126     StructuredTraces.as_label_of_pc = (fun pc ->
    127     BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    128       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    129       Nat.O)))))))))))))))) (Obj.magic pc) cost_labels);
    130     StructuredTraces.as_result = (fun x -> assert false (* absurd case *));
    131     StructuredTraces.as_call_ident = (fun x -> assert false
    132     (* absurd case *)); StructuredTraces.as_tailcall_ident = (fun x ->
    133     assert false (* absurd case *)) }
     216  StructuredTraces.as_pc_of =
     217  (Obj.magic (Status.program_counter (Fetch.load_code_memory prog.ASM.oc)));
     218  StructuredTraces.as_classify =
     219  (Obj.magic (AbstractStatus.oC_classify code_memory));
     220  StructuredTraces.as_label_of_pc = (fun pc ->
     221  BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     222    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     223    Nat.O)))))))))))))))) (Obj.magic pc) prog.ASM.costlabels);
     224  StructuredTraces.as_result = (fun st ->
     225  as_result_of_finaladdr (Fetch.load_code_memory prog.ASM.oc) (Obj.magic st)
     226    prog.ASM.final_pc); StructuredTraces.as_call_ident = (fun x ->
     227  Positive.One (* absurd case *)); StructuredTraces.as_tailcall_ident =
     228  (fun x -> assert false (* absurd case *)) }
    134229
    135230(** val trace_any_label_length :
    136     BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    137     BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
     231    ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
    138232    Status.status -> Status.status -> StructuredTraces.trace_any_label ->
    139233    Nat.nat **)
    140 let trace_any_label_length code_memory cost_labels trace_ends_flag start_status final_status the_trace =
    141   StructuredTraces.as_trace_any_label_length'
    142     (oC_abstract_status code_memory cost_labels) trace_ends_flag
    143     (Obj.magic start_status) (Obj.magic final_status) the_trace
     234let trace_any_label_length prog =
     235  let code_memory = Fetch.load_code_memory prog.ASM.oc in
     236  (fun trace_ends_flag start_status final_status the_trace ->
     237  StructuredTraces.as_trace_any_label_length' (oC_abstract_status prog)
     238    trace_ends_flag (Obj.magic start_status) (Obj.magic final_status)
     239    the_trace)
    144240
    145241(** val all_program_counter_list :
     
    154250
    155251(** val compute_paid_trace_any_label :
    156     BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    157     BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
     252    ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
    158253    Status.status -> Status.status -> StructuredTraces.trace_any_label ->
    159254    Nat.nat **)
    160 let rec compute_paid_trace_any_label code_memory cost_labels trace_ends_flag start_status final_status = function
     255let rec compute_paid_trace_any_label prog trace_ends_flag start_status final_status = function
    161256| StructuredTraces.Tal_base_not_return (the_status, x) ->
    162   Interpret.current_instruction_cost code_memory (Obj.magic the_status)
     257  Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
     258    (Obj.magic the_status)
    163259| StructuredTraces.Tal_base_return (the_status, x) ->
    164   Interpret.current_instruction_cost code_memory (Obj.magic the_status)
     260  Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
     261    (Obj.magic the_status)
    165262| StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) ->
    166   Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
     263  Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
     264    (Obj.magic pre_fun_call)
    167265| StructuredTraces.Tal_base_tailcall
    168266    (pre_fun_call, start_fun_call, final, x1) ->
    169   Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
     267  Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
     268    (Obj.magic pre_fun_call)
    170269| StructuredTraces.Tal_step_call
    171270    (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
    172271     call_trace, final_trace) ->
    173272  let current_instruction_cost =
    174     Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
     273    Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
     274      (Obj.magic pre_fun_call)
    175275  in
    176276  let final_trace_cost =
    177     compute_paid_trace_any_label code_memory cost_labels end_flag
    178       (Obj.magic after_fun_call) (Obj.magic final) final_trace
     277    compute_paid_trace_any_label prog end_flag (Obj.magic after_fun_call)
     278      (Obj.magic final) final_trace
    179279  in
    180280  Nat.plus current_instruction_cost final_trace_cost
     
    182282    (end_flag, status_pre, status_init, status_end, tail_trace) ->
    183283  let current_instruction_cost =
    184     Interpret.current_instruction_cost code_memory (Obj.magic status_pre)
     284    Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
     285      (Obj.magic status_pre)
    185286  in
    186287  let tail_trace_cost =
    187     compute_paid_trace_any_label code_memory cost_labels end_flag
    188       (Obj.magic status_init) (Obj.magic status_end) tail_trace
     288    compute_paid_trace_any_label prog end_flag (Obj.magic status_init)
     289      (Obj.magic status_end) tail_trace
    189290  in
    190291  Nat.plus current_instruction_cost tail_trace_cost
    191292
    192293(** val compute_paid_trace_label_label :
    193     BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    194     BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
     294    ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
    195295    Status.status -> Status.status -> StructuredTraces.trace_label_label ->
    196296    Nat.nat **)
    197 let compute_paid_trace_label_label code_memory cost_labels trace_ends_flag start_status final_status = function
    198 | StructuredTraces.Tll_base (ends_flag, initial, final, given_trace) ->
    199   compute_paid_trace_any_label code_memory cost_labels ends_flag
    200     (Obj.magic initial) (Obj.magic final) given_trace
     297let compute_paid_trace_label_label prog =
     298  let code_memory = Fetch.load_code_memory prog.ASM.oc in
     299  (fun trace_ends_flag start_status final_status the_trace ->
     300  let StructuredTraces.Tll_base (ends_flag, initial, final, given_trace) =
     301    the_trace
     302  in
     303  compute_paid_trace_any_label prog ends_flag (Obj.magic initial)
     304    (Obj.magic final) given_trace)
    201305
    202306(** val block_cost' :
    203     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat
    204     -> CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Bool.bool ->
     307    ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Bool.bool ->
    205308    Nat.nat Types.sig0 **)
    206 let rec block_cost' code_memory' program_counter' program_size cost_labels first_time_around =
     309let rec block_cost' prog program_counter' program_size first_time_around =
     310  let code_memory' = Fetch.load_code_memory prog.ASM.oc in
    207311  (match program_size with
    208312   | Nat.O -> (fun _ -> Nat.O)
    209313   | Nat.S program_size' ->
    210314     (fun _ ->
    211        (let { Types.fst = eta31808; Types.snd = ticks } =
    212           Fetch.fetch code_memory' program_counter'
     315       (let { Types.fst = eta31815; Types.snd = ticks } =
     316          Fetch.fetch (Fetch.load_code_memory prog.ASM.oc) program_counter'
    213317        in
    214318       let { Types.fst = instruction; Types.snd = program_counter'' } =
    215          eta31808
     319         eta31815
    216320       in
    217321       (fun _ ->
     
    220324                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    221325                 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter'
    222                  cost_labels with
     326                 prog.ASM.costlabels with
    223327         | Types.None -> Bool.True
    224328         | Types.Some x -> first_time_around
     
    234338                      Nat.plus ticks
    235339                        (Types.pi1
    236                           (block_cost' code_memory' program_counter''
    237                             program_size' cost_labels Bool.False)))
     340                          (block_cost' prog program_counter'' program_size'
     341                            Bool.False)))
    238342                  | ASM.LCALL addr ->
    239343                    (fun _ ->
    240344                      Nat.plus ticks
    241345                        (Types.pi1
    242                           (block_cost' code_memory' program_counter''
    243                             program_size' cost_labels Bool.False)))
     346                          (block_cost' prog program_counter'' program_size'
     347                            Bool.False)))
    244348                  | ASM.AJMP addr ->
    245349                    (fun _ ->
     
    250354                      Nat.plus ticks
    251355                        (Types.pi1
    252                           (block_cost' code_memory' jump_target program_size'
    253                             cost_labels Bool.False)))
     356                          (block_cost' prog jump_target program_size'
     357                            Bool.False)))
    254358                  | ASM.LJMP addr ->
    255359                    (fun _ ->
     
    260364                      Nat.plus ticks
    261365                        (Types.pi1
    262                           (block_cost' code_memory' jump_target program_size'
    263                             cost_labels Bool.False)))
     366                          (block_cost' prog jump_target program_size'
     367                            Bool.False)))
    264368                  | ASM.SJMP addr ->
    265369                    (fun _ ->
     
    270374                      Nat.plus ticks
    271375                        (Types.pi1
    272                           (block_cost' code_memory' jump_target program_size'
    273                             cost_labels Bool.False)))
     376                          (block_cost' prog jump_target program_size'
     377                            Bool.False)))
    274378                  | ASM.MOVC (src, trgt) ->
    275379                    (fun _ ->
    276380                      Nat.plus ticks
    277381                        (Types.pi1
    278                           (block_cost' code_memory' program_counter''
    279                             program_size' cost_labels Bool.False)))
     382                          (block_cost' prog program_counter'' program_size'
     383                            Bool.False)))
    280384                  | ASM.RealInstruction real_instruction ->
    281385                    (fun _ ->
     
    285389                           Nat.plus ticks
    286390                             (Types.pi1
    287                                (block_cost' code_memory' program_counter''
    288                                  program_size' cost_labels Bool.False)))
     391                               (block_cost' prog program_counter''
     392                                 program_size' Bool.False)))
    289393                       | ASM.ADDC (x, x0) ->
    290394                         (fun _ ->
    291395                           Nat.plus ticks
    292396                             (Types.pi1
    293                                (block_cost' code_memory' program_counter''
    294                                  program_size' cost_labels Bool.False)))
     397                               (block_cost' prog program_counter''
     398                                 program_size' Bool.False)))
    295399                       | ASM.SUBB (x, x0) ->
    296400                         (fun _ ->
    297401                           Nat.plus ticks
    298402                             (Types.pi1
    299                                (block_cost' code_memory' program_counter''
    300                                  program_size' cost_labels Bool.False)))
     403                               (block_cost' prog program_counter''
     404                                 program_size' Bool.False)))
    301405                       | ASM.INC x ->
    302406                         (fun _ ->
    303407                           Nat.plus ticks
    304408                             (Types.pi1
    305                                (block_cost' code_memory' program_counter''
    306                                  program_size' cost_labels Bool.False)))
     409                               (block_cost' prog program_counter''
     410                                 program_size' Bool.False)))
    307411                       | ASM.DEC x ->
    308412                         (fun _ ->
    309413                           Nat.plus ticks
    310414                             (Types.pi1
    311                                (block_cost' code_memory' program_counter''
    312                                  program_size' cost_labels Bool.False)))
     415                               (block_cost' prog program_counter''
     416                                 program_size' Bool.False)))
    313417                       | ASM.MUL (x, x0) ->
    314418                         (fun _ ->
    315419                           Nat.plus ticks
    316420                             (Types.pi1
    317                                (block_cost' code_memory' program_counter''
    318                                  program_size' cost_labels Bool.False)))
     421                               (block_cost' prog program_counter''
     422                                 program_size' Bool.False)))
    319423                       | ASM.DIV (x, x0) ->
    320424                         (fun _ ->
    321425                           Nat.plus ticks
    322426                             (Types.pi1
    323                                (block_cost' code_memory' program_counter''
    324                                  program_size' cost_labels Bool.False)))
     427                               (block_cost' prog program_counter''
     428                                 program_size' Bool.False)))
    325429                       | ASM.DA x ->
    326430                         (fun _ ->
    327431                           Nat.plus ticks
    328432                             (Types.pi1
    329                                (block_cost' code_memory' program_counter''
    330                                  program_size' cost_labels Bool.False)))
     433                               (block_cost' prog program_counter''
     434                                 program_size' Bool.False)))
    331435                       | ASM.JC relative -> (fun _ -> ticks)
    332436                       | ASM.JNC relative -> (fun _ -> ticks)
     
    342446                           Nat.plus ticks
    343447                             (Types.pi1
    344                                (block_cost' code_memory' program_counter''
    345                                  program_size' cost_labels Bool.False)))
     448                               (block_cost' prog program_counter''
     449                                 program_size' Bool.False)))
    346450                       | ASM.ORL x ->
    347451                         (fun _ ->
    348452                           Nat.plus ticks
    349453                             (Types.pi1
    350                                (block_cost' code_memory' program_counter''
    351                                  program_size' cost_labels Bool.False)))
     454                               (block_cost' prog program_counter''
     455                                 program_size' Bool.False)))
    352456                       | ASM.XRL x ->
    353457                         (fun _ ->
    354458                           Nat.plus ticks
    355459                             (Types.pi1
    356                                (block_cost' code_memory' program_counter''
    357                                  program_size' cost_labels Bool.False)))
     460                               (block_cost' prog program_counter''
     461                                 program_size' Bool.False)))
    358462                       | ASM.CLR x ->
    359463                         (fun _ ->
    360464                           Nat.plus ticks
    361465                             (Types.pi1
    362                                (block_cost' code_memory' program_counter''
    363                                  program_size' cost_labels Bool.False)))
     466                               (block_cost' prog program_counter''
     467                                 program_size' Bool.False)))
    364468                       | ASM.CPL x ->
    365469                         (fun _ ->
    366470                           Nat.plus ticks
    367471                             (Types.pi1
    368                                (block_cost' code_memory' program_counter''
    369                                  program_size' cost_labels Bool.False)))
     472                               (block_cost' prog program_counter''
     473                                 program_size' Bool.False)))
    370474                       | ASM.RL x ->
    371475                         (fun _ ->
    372476                           Nat.plus ticks
    373477                             (Types.pi1
    374                                (block_cost' code_memory' program_counter''
    375                                  program_size' cost_labels Bool.False)))
     478                               (block_cost' prog program_counter''
     479                                 program_size' Bool.False)))
    376480                       | ASM.RLC x ->
    377481                         (fun _ ->
    378482                           Nat.plus ticks
    379483                             (Types.pi1
    380                                (block_cost' code_memory' program_counter''
    381                                  program_size' cost_labels Bool.False)))
     484                               (block_cost' prog program_counter''
     485                                 program_size' Bool.False)))
    382486                       | ASM.RR x ->
    383487                         (fun _ ->
    384488                           Nat.plus ticks
    385489                             (Types.pi1
    386                                (block_cost' code_memory' program_counter''
    387                                  program_size' cost_labels Bool.False)))
     490                               (block_cost' prog program_counter''
     491                                 program_size' Bool.False)))
    388492                       | ASM.RRC x ->
    389493                         (fun _ ->
    390494                           Nat.plus ticks
    391495                             (Types.pi1
    392                                (block_cost' code_memory' program_counter''
    393                                  program_size' cost_labels Bool.False)))
     496                               (block_cost' prog program_counter''
     497                                 program_size' Bool.False)))
    394498                       | ASM.SWAP x ->
    395499                         (fun _ ->
    396500                           Nat.plus ticks
    397501                             (Types.pi1
    398                                (block_cost' code_memory' program_counter''
    399                                  program_size' cost_labels Bool.False)))
     502                               (block_cost' prog program_counter''
     503                                 program_size' Bool.False)))
    400504                       | ASM.MOV x ->
    401505                         (fun _ ->
    402506                           Nat.plus ticks
    403507                             (Types.pi1
    404                                (block_cost' code_memory' program_counter''
    405                                  program_size' cost_labels Bool.False)))
     508                               (block_cost' prog program_counter''
     509                                 program_size' Bool.False)))
    406510                       | ASM.MOVX x ->
    407511                         (fun _ ->
    408512                           Nat.plus ticks
    409513                             (Types.pi1
    410                                (block_cost' code_memory' program_counter''
    411                                  program_size' cost_labels Bool.False)))
     514                               (block_cost' prog program_counter''
     515                                 program_size' Bool.False)))
    412516                       | ASM.SETB x ->
    413517                         (fun _ ->
    414518                           Nat.plus ticks
    415519                             (Types.pi1
    416                                (block_cost' code_memory' program_counter''
    417                                  program_size' cost_labels Bool.False)))
     520                               (block_cost' prog program_counter''
     521                                 program_size' Bool.False)))
    418522                       | ASM.PUSH x ->
    419523                         (fun _ ->
    420524                           Nat.plus ticks
    421525                             (Types.pi1
    422                                (block_cost' code_memory' program_counter''
    423                                  program_size' cost_labels Bool.False)))
     526                               (block_cost' prog program_counter''
     527                                 program_size' Bool.False)))
    424528                       | ASM.POP x ->
    425529                         (fun _ ->
    426530                           Nat.plus ticks
    427531                             (Types.pi1
    428                                (block_cost' code_memory' program_counter''
    429                                  program_size' cost_labels Bool.False)))
     532                               (block_cost' prog program_counter''
     533                                 program_size' Bool.False)))
    430534                       | ASM.XCH (x, x0) ->
    431535                         (fun _ ->
    432536                           Nat.plus ticks
    433537                             (Types.pi1
    434                                (block_cost' code_memory' program_counter''
    435                                  program_size' cost_labels Bool.False)))
     538                               (block_cost' prog program_counter''
     539                                 program_size' Bool.False)))
    436540                       | ASM.XCHD (x, x0) ->
    437541                         (fun _ ->
    438542                           Nat.plus ticks
    439543                             (Types.pi1
    440                                (block_cost' code_memory' program_counter''
    441                                  program_size' cost_labels Bool.False)))
     544                               (block_cost' prog program_counter''
     545                                 program_size' Bool.False)))
    442546                       | ASM.RET -> (fun _ -> ticks)
    443547                       | ASM.RETI -> (fun _ -> ticks)
     
    446550                           Nat.plus ticks
    447551                             (Types.pi1
    448                                (block_cost' code_memory' program_counter''
    449                                  program_size' cost_labels Bool.False)))
     552                               (block_cost' prog program_counter''
     553                                 program_size' Bool.False)))
    450554                       | ASM.JMP addr ->
    451555                         (fun _ ->
    452556                           Nat.plus ticks
    453557                             (Types.pi1
    454                                (block_cost' code_memory' program_counter''
    455                                  program_size' cost_labels Bool.False)))) __))
    456                   __))
     558                               (block_cost' prog program_counter''
     559                                 program_size' Bool.False)))) __)) __))
    457560          | Bool.False -> (fun _ -> Nat.O)) __
    458561       in
     
    460563
    461564(** val block_cost :
    462     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
    463     CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Nat.nat Types.sig0 **)
    464 let block_cost code_memory program_counter cost_labels =
     565    ASM.labelled_object_code -> BitVector.word -> Nat.nat Types.sig0 **)
     566let block_cost prog program_counter =
    465567  let cost_of_block =
    466     block_cost' code_memory program_counter
     568    block_cost' prog program_counter
    467569      (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    468570        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    469         (Nat.S Nat.O))))))))))))))))) cost_labels Bool.True
     571        (Nat.S Nat.O))))))))))))))))) Bool.True
    470572  in
    471573  cost_of_block
  • extracted/aSMCosts.mli

    r2905 r2909  
    115115open Interpret
    116116
     117val aSMRegisterRets : ASM.subaddressing_mode List.list
     118
     119val as_result_of_finaladdr :
     120  'a1 -> 'a1 Status.preStatus -> BitVector.word -> Integers.int Types.option
     121
    117122val oC_abstract_status :
    118   BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    119   BitVectorTrie.bitVectorTrie -> StructuredTraces.abstract_status
     123  ASM.labelled_object_code -> StructuredTraces.abstract_status
    120124
    121125val trace_any_label_length :
    122   BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    123   BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
     126  ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
    124127  Status.status -> Status.status -> StructuredTraces.trace_any_label ->
    125128  Nat.nat
     
    128131
    129132val compute_paid_trace_any_label :
    130   BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    131   BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
     133  ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
    132134  Status.status -> Status.status -> StructuredTraces.trace_any_label ->
    133135  Nat.nat
    134136
    135137val compute_paid_trace_label_label :
    136   BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    137   BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
     138  ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
    138139  Status.status -> Status.status -> StructuredTraces.trace_label_label ->
    139140  Nat.nat
    140141
    141142val block_cost' :
    142   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat ->
    143   CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Bool.bool -> Nat.nat
    144   Types.sig0
     143  ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Bool.bool ->
     144  Nat.nat Types.sig0
    145145
    146146val block_cost :
    147   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
    148   CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Nat.nat Types.sig0
     147  ASM.labelled_object_code -> BitVector.word -> Nat.nat Types.sig0
    149148
  • extracted/aSMCostsSplit.ml

    r2905 r2909  
    120120
    121121(** val traverse_code_internal :
    122     BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    123     BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat -> Nat.nat
     122    ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Nat.nat
    124123    Identifiers.identifier_map Types.sig0 **)
    125 let rec traverse_code_internal code_memory cost_labels program_counter program_size =
     124let rec traverse_code_internal prog program_counter program_size =
    126125  (match program_size with
    127126   | Nat.O -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag)
     
    138137       in
    139138       let cost_mapping =
    140          traverse_code_internal code_memory cost_labels new_program_counter'
    141            program_size'
     139         traverse_code_internal prog new_program_counter' program_size'
    142140       in
    143141       (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    144142                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    145143                (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter
    146                 cost_labels with
     144                prog.ASM.costlabels with
    147145        | Types.None -> (fun _ -> Types.pi1 cost_mapping)
    148146        | Types.Some lbl ->
    149147          (fun _ ->
    150             let cost =
    151               ASMCosts.block_cost code_memory program_counter cost_labels
    152             in
     148            let cost = ASMCosts.block_cost prog program_counter in
    153149            Identifiers.add PreIdentifiers.CostTag (Types.pi1 cost_mapping)
    154150              lbl (Types.pi1 cost))) __)) __
    155151
    156152(** val traverse_code :
    157     BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    158     BitVectorTrie.bitVectorTrie -> Nat.nat Identifiers.identifier_map
    159     Types.sig0 **)
    160 let traverse_code code_memory cost_labels =
     153    ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **)
     154let traverse_code prog =
    161155  Types.pi1
    162     (traverse_code_internal code_memory cost_labels
     156    (traverse_code_internal prog
    163157      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    164158        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    169163
    170164(** val compute_costs :
    171     ASM.object_code -> CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
    172     Nat.nat Identifiers.identifier_map Types.sig0 **)
    173 let compute_costs program cost_labels =
    174   let code_memory = Fetch.load_code_memory program in
    175   traverse_code code_memory cost_labels
     165    ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **)
     166let compute_costs =
     167  traverse_code
    176168
    177169(** val aSM_cost_map :
    178170    ASM.labelled_object_code -> StructuredTraces.as_cost_map **)
    179171let aSM_cost_map p =
    180   let cost_map = compute_costs p.ASM.oc p.ASM.costlabels in
     172  let cost_map = compute_costs p in
    181173  (fun l_sig ->
    182174  Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map)
    183     (StructuredTraces.as_cost_get_label
    184       (ASMCosts.oC_abstract_status (Fetch.load_code_memory p.ASM.oc)
    185         p.ASM.costlabels) l_sig))
     175    (StructuredTraces.as_cost_get_label (ASMCosts.oC_abstract_status p)
     176      l_sig))
    186177
  • extracted/aSMCostsSplit.mli

    r2773 r2909  
    120120
    121121val traverse_code_internal :
    122   BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    123   BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat -> Nat.nat
     122  ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Nat.nat
    124123  Identifiers.identifier_map Types.sig0
    125124
    126125val traverse_code :
    127   BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    128   BitVectorTrie.bitVectorTrie -> Nat.nat Identifiers.identifier_map
    129   Types.sig0
     126  ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0
    130127
    131128val compute_costs :
    132   ASM.object_code -> CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
    133   Nat.nat Identifiers.identifier_map Types.sig0
     129  ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0
    134130
    135131val aSM_cost_map : ASM.labelled_object_code -> StructuredTraces.as_cost_map
  • 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;
  • extracted/compiler.mli

    r2875 r2909  
    367367
    368368val lift_cost_map_back_to_front :
    369   Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
    370   CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
     369  Csyntax.clight_program -> ASM.labelled_object_code ->
    371370  StructuredTraces.as_cost_map -> Label.clight_cost_map
    372371
  • extracted/interpret.ml

    r2908 r2909  
    348348                  (Nat.S (Nat.S Nat.O))))))))) carry
    349349            in
    350             let s0 = Status.set_8051_sfr cm s' Status.SFR_DPL bl in
    351             Status.set_8051_sfr cm s0 Status.SFR_DPH bu)
     350            let s'' = Status.set_8051_sfr cm s' Status.SFR_DPL bl in
     351            Status.set_8051_sfr cm s'' Status.SFR_DPH bu)
    352352        | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
    353353        | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
  • extracted/interpret2.ml

    r2905 r2909  
    163163    ASM.labelled_object_code -> Measurable.preclassified_system **)
    164164let oC_preclassified_system c =
    165   let cm = Fetch.load_code_memory c.ASM.oc in
    166   mk_preclassified_system_of_abstract_status
    167     (ASMCosts.oC_abstract_status cm c.ASM.costlabels) (fun st ->
     165  mk_preclassified_system_of_abstract_status (ASMCosts.oC_abstract_status c)
     166    (fun st ->
    168167    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
    169168      (Interpret.execute_1 (Fetch.load_code_memory c.ASM.oc) (Obj.magic st)))
    170     (Obj.magic (Status.initialise_status cm))
     169    (Obj.magic (Status.initialise_status (Fetch.load_code_memory c.ASM.oc)))
    171170
    172171open Assembly
     
    213212  | ASM.Mov (x, x0) -> Types.None
    214213
     214(** val aSM_as_result :
     215    ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int
     216    Types.option **)
     217let aSM_as_result prog st =
     218  let finaladdr =
     219    Fetch.address_of_word_labels prog.ASM.code prog.ASM.final_label
     220  in
     221  ASMCosts.as_result_of_finaladdr prog st finaladdr
     222
    215223(** val aSM_abstract_status :
    216224    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     
    221229    StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
    222230    StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
    223     StructuredTraces.as_result = (fun x -> Types.None);
     231    StructuredTraces.as_result = (Obj.magic (aSM_as_result prog));
    224232    StructuredTraces.as_call_ident = (fun x -> Positive.One
    225233    (* absurd case *)); StructuredTraces.as_tailcall_ident = (fun x ->
  • extracted/interpret2.mli

    r2905 r2909  
    155155  Types.option
    156156
     157val aSM_as_result :
     158  ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int
     159  Types.option
     160
    157161val aSM_abstract_status :
    158162  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
  • extracted/semantics.ml

    r2905 r2909  
    449449| Compiler.Assembly_pass ->
    450450  (fun prog ->
    451     let { Types.fst = eta32145; Types.snd = policy } = Obj.magic prog in
    452     let { Types.fst = code; Types.snd = sigma } = eta32145 in
     451    let { Types.fst = eta32152; Types.snd = policy } = Obj.magic prog in
     452    let { Types.fst = code; Types.snd = sigma } = eta32152 in
    453453    Interpret2.aSM_preclassified_system code sigma policy)
    454454| Compiler.Object_code_pass ->
Note: See TracChangeset for help on using the changeset viewer.