source: extracted/aSMCostsSplit.ml @ 3009

Last change on this file since 3009 was 2997, checked in by sacerdot, 7 years ago

New extraction.

File size: 3.3 KB
RevLine 
[2601]1open Preamble
2
[2773]3open Fetch
[2601]4
[2773]5open Hide
[2601]6
[2773]7open Division
[2601]8
[2773]9open Z
[2601]10
[2773]11open BitVectorZ
12
13open Pointers
14
15open Coqlib
16
17open Values
18
19open Events
20
21open IOMonad
22
23open IO
24
[2601]25open Sets
26
27open Listb
28
[2773]29open StructuredTraces
[2601]30
[2773]31open AbstractStatus
[2601]32
[2773]33open BitVectorTrie
34
[2649]35open String
36
[2717]37open Exp
38
[2601]39open Arithmetic
40
[2773]41open Vector
42
43open FoldStuff
44
45open BitVector
46
47open Extranat
48
[2601]49open Integers
50
51open AST
52
[2773]53open LabelledObjects
[2601]54
55open Proper
56
57open PositiveMap
58
59open Deqsets
60
[2649]61open ErrorMessages
62
[2601]63open PreIdentifiers
64
65open Errors
66
67open Extralib
68
69open Setoids
70
71open Monad
72
73open Option
74
75open Div_and_mod
76
77open Jmeq
78
79open Russell
80
[2773]81open Util
[2601]82
83open List
84
[2773]85open Lists
[2601]86
87open Bool
88
[2773]89open Relations
90
91open Nat
92
93open Positive
94
[2601]95open Hints_declaration
96
97open Core_notation
98
99open Pts
100
101open Logic
102
[2773]103open Types
[2601]104
[2773]105open Identifiers
[2601]106
[2773]107open CostLabel
[2601]108
109open ASM
110
[2773]111open Status
112
113open StatusProofs
114
115open Interpret
116
[2601]117open ASMCosts
118
119open UtilBranch
120
121(** val traverse_code_internal :
[2909]122    ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Nat.nat
[2601]123    Identifiers.identifier_map Types.sig0 **)
[2909]124let rec traverse_code_internal prog program_counter program_size =
[2601]125  (match program_size with
[2997]126   | Nat.O -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag)
127   | Nat.S program_size' ->
[2601]128     (fun _ ->
129       let new_program_counter' =
130         Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
131           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
132           Nat.O))))))))))))))))
133           (Arithmetic.bitvector_of_nat (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
135             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O))
[2773]136           program_counter
[2601]137       in
138       let cost_mapping =
[2909]139         traverse_code_internal prog new_program_counter' program_size'
[2601]140       in
141       (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
142                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
[2773]143                (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter
[2909]144                prog.ASM.costlabels with
[2601]145        | Types.None -> (fun _ -> Types.pi1 cost_mapping)
146        | Types.Some lbl ->
147          (fun _ ->
[2909]148            let cost = ASMCosts.block_cost prog program_counter in
[2649]149            Identifiers.add PreIdentifiers.CostTag (Types.pi1 cost_mapping)
150              lbl (Types.pi1 cost))) __)) __
[2601]151
152(** val traverse_code :
[2909]153    ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **)
154let traverse_code prog =
[2601]155  Types.pi1
[2909]156    (traverse_code_internal prog
[2601]157      (BitVector.zero (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)))))))))))))))))
[2997]160      (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
161        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
162        (Nat.S Nat.O))))))))))))))))))
[2601]163
164(** val compute_costs :
[2909]165    ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **)
166let compute_costs =
167  traverse_code
[2601]168
169(** val aSM_cost_map :
[2773]170    ASM.labelled_object_code -> StructuredTraces.as_cost_map **)
[2601]171let aSM_cost_map p =
[2909]172  let cost_map = compute_costs p in
[2601]173  (fun l_sig ->
[2649]174  Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map)
[2909]175    (StructuredTraces.as_cost_get_label (ASMCosts.oC_abstract_status p)
176      l_sig))
[2601]177
Note: See TracBrowser for help on using the repository browser.