source: driver/extracted/costInj.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: 2.2 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
109(** val reverse_label_map :
110    RTLabs_syntax.statement Graphs.graph -> PreIdentifiers.identifier
111    Identifiers.identifier_map Types.option **)
112let reverse_label_map g =
113  Identifiers.foldi PreIdentifiers.LabelTag (fun l s m ->
114    match m with
115    | Types.None -> Types.None
116    | Types.Some m0 ->
117      (match CostSpec.cost_label_of s with
118       | Types.None -> Types.Some m0
119       | Types.Some cl ->
120         (match Identifiers.lookup PreIdentifiers.CostTag m0 cl with
121          | Types.None ->
122            Types.Some (Identifiers.add PreIdentifiers.CostTag m0 cl l)
123          | Types.Some x -> Types.None))) g (Types.Some
124    (Identifiers.empty_map PreIdentifiers.CostTag))
125
126(** val check_fun_inj : RTLabs_syntax.internal_function -> Bool.bool **)
127let check_fun_inj f =
128  match reverse_label_map f.RTLabs_syntax.f_graph with
129  | Types.None -> Bool.False
130  | Types.Some x -> Bool.True
131
132(** val check_program_cost_injectivity :
133    RTLabs_syntax.rTLabs_program -> Bool.bool **)
134let check_program_cost_injectivity p =
135  Lists.all (fun x ->
136    match x.Types.snd with
137    | AST.Internal f -> check_fun_inj f
138    | AST.External x0 -> Bool.True) p.AST.prog_funct
139
140(** val check_program_cost_injectivity_prf :
141    RTLabs_syntax.rTLabs_program -> __ Errors.res **)
142let check_program_cost_injectivity_prf p =
143  (match check_program_cost_injectivity p with
144   | Bool.True -> (fun _ -> Errors.OK __)
145   | Bool.False ->
146     (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadCostLabelling))) __
147
Note: See TracBrowser for help on using the repository browser.