source: driver/extracted/costCheck.ml @ 3106

Last change on this file since 3106 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 5.4 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open Graphs
6
7open Order
8
9open Registers
10
11open FrontEndVal
12
13open Hide
14
15open ByteValues
16
17open GenMem
18
19open FrontEndMem
20
21open Division
22
23open Z
24
25open BitVectorZ
26
27open Pointers
28
29open Coqlib
30
31open Values
32
33open FrontEndOps
34
35open CostLabel
36
37open Proper
38
39open PositiveMap
40
41open Deqsets
42
43open ErrorMessages
44
45open PreIdentifiers
46
47open Errors
48
49open Extralib
50
51open Lists
52
53open Positive
54
55open Identifiers
56
57open Exp
58
59open Arithmetic
60
61open Vector
62
63open Div_and_mod
64
65open Util
66
67open FoldStuff
68
69open BitVector
70
71open Jmeq
72
73open Russell
74
75open List
76
77open Setoids
78
79open Monad
80
81open Option
82
83open Extranat
84
85open Bool
86
87open Relations
88
89open Nat
90
91open Integers
92
93open Types
94
95open AST
96
97open Hints_declaration
98
99open Core_notation
100
101open Pts
102
103open Logic
104
105open RTLabs_syntax
106
107open CostSpec
108
109open Extra_bool
110
111open Sets
112
113open Listb
114
115open Listb_extra
116
117open CostMisc
118
119(** val check_well_cost_fn : RTLabs_syntax.internal_function -> Bool.bool **)
120let check_well_cost_fn f =
121  Bool.andb
122    (Identifiers.idmap_all PreIdentifiers.LabelTag f.RTLabs_syntax.f_graph
123      (fun l s _ ->
124      CostSpec.well_cost_labelled_statement f.RTLabs_syntax.f_graph s))
125    (CostSpec.is_cost_label
126      (Identifiers.lookup_present PreIdentifiers.LabelTag
127        f.RTLabs_syntax.f_graph (Types.pi1 f.RTLabs_syntax.f_entry)))
128
129open Deqsets_extra
130
131(** val check_label_bounded :
132    RTLabs_syntax.statement Graphs.graph -> Graphs.label -> Graphs.label
133    List.list -> Identifiers.identifier_set -> Nat.nat ->
134    Identifiers.identifier_set Types.option **)
135let rec check_label_bounded g checking checking_tail to_check term_check =
136  let stop_now = Types.Some to_check in
137  (match term_check with
138   | Nat.O -> (fun _ -> assert false (* absurd case *))
139   | Nat.S term_check' ->
140     (fun _ ->
141       let st = Identifiers.lookup_present PreIdentifiers.LabelTag g checking
142       in
143       let succs = CostSpec.successors st in
144       (match succs with
145        | List.Nil -> (fun _ -> stop_now)
146        | List.Cons (h, t) ->
147          (match t with
148           | List.Nil ->
149             (fun _ ->
150               let st' =
151                 Identifiers.lookup_present PreIdentifiers.LabelTag g h
152               in
153               (match CostSpec.is_cost_label st' with
154                | Bool.True -> stop_now
155                | Bool.False ->
156                  (match Identifiers.try_remove PreIdentifiers.LabelTag
157                           to_check h with
158                   | Types.None ->
159                     (fun _ ->
160                       match Bool.orb
161                               (Deqsets.eqb
162                                 (Identifiers.deq_identifier
163                                   PreIdentifiers.LabelTag) (Obj.magic h)
164                                 (Obj.magic checking))
165                               (Listb.memb
166                                 (Identifiers.deq_identifier
167                                   PreIdentifiers.LabelTag) (Obj.magic h)
168                                 (Obj.magic checking_tail)) with
169                       | Bool.True -> Types.None
170                       | Bool.False -> stop_now)
171                   | Types.Some to_check' ->
172                     (fun _ ->
173                       check_label_bounded g h (List.Cons (checking,
174                         checking_tail)) to_check'.Types.snd term_check')) __))
175           | List.Cons (x, x0) -> (fun _ -> stop_now))) __)) __
176
177(** val check_graph_bounded :
178    RTLabs_syntax.statement Graphs.graph -> Identifiers.identifier_set ->
179    Graphs.label -> Nat.nat -> Bool.bool **)
180let rec check_graph_bounded g to_check start term_check =
181  (match term_check with
182   | Nat.O -> (fun _ -> assert false (* absurd case *))
183   | Nat.S term_check' ->
184     (fun _ ->
185       (match check_label_bounded g start List.Nil to_check
186                (Identifiers.id_map_size PreIdentifiers.LabelTag g) with
187        | Types.None -> (fun _ -> Bool.False)
188        | Types.Some to_check' ->
189          (fun _ ->
190            (match Identifiers.choose PreIdentifiers.LabelTag to_check' with
191             | Types.None -> (fun _ _ _ -> Bool.True)
192             | Types.Some l_to_check'' ->
193               (fun _ _ _ ->
194                 check_graph_bounded g l_to_check''.Types.snd
195                   l_to_check''.Types.fst.Types.fst term_check')) __ __ __))
196         __)) __
197
198(** val check_sound_cost_fn :
199    RTLabs_syntax.internal_function -> Bool.bool **)
200let check_sound_cost_fn fn =
201  (match Identifiers.try_remove PreIdentifiers.LabelTag
202           (Identifiers.id_set_of_map PreIdentifiers.LabelTag
203             fn.RTLabs_syntax.f_graph) (Types.pi1 fn.RTLabs_syntax.f_entry) with
204   | Types.None -> (fun _ -> assert false (* absurd case *))
205   | Types.Some to_check ->
206     (fun _ _ _ ->
207       check_graph_bounded fn.RTLabs_syntax.f_graph to_check.Types.snd
208         (Types.pi1 fn.RTLabs_syntax.f_entry)
209         (Identifiers.id_map_size PreIdentifiers.LabelTag
210           fn.RTLabs_syntax.f_graph))) __ __ __
211
212(** val check_cost_program : RTLabs_syntax.rTLabs_program -> Bool.bool **)
213let check_cost_program p =
214  Lists.all (fun fn ->
215    match fn.Types.snd with
216    | AST.Internal fn0 ->
217      Bool.andb (check_well_cost_fn fn0) (check_sound_cost_fn fn0)
218    | AST.External x -> Bool.True) p.AST.prog_funct
219
220(** val check_cost_program_prf :
221    RTLabs_syntax.rTLabs_program -> __ Errors.res **)
222let check_cost_program_prf p =
223  (match check_cost_program p with
224   | Bool.True -> (fun _ -> Errors.OK __)
225   | Bool.False ->
226     (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadCostLabelling))) __
227
Note: See TracBrowser for help on using the repository browser.