1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2010-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
(* Conditions inside logs, a simplified Constraint module *)
open ConstrGen
open Printf
type cond = (MiscParser.location,ToolsConstant.v,MiscParser.fault_type) prop constr
let foralltrue = ForallStates (And [])
module SL = StateLexer.Make(struct let debug = false end)
let rec tr_v v =
let open Constant in
match v with
| Concrete i -> Concrete (Int64.of_string i)
| ConcreteVector vs -> ConcreteVector (List.map tr_v vs)
| ConcreteRecord vs -> ConcreteRecord (StringMap.map tr_v vs)
| Symbolic _|Label _|Tag _
| PteVal _|Instruction _|Frozen _
as w -> w
let tr_atom = function
| LV(loc,v) -> LV(loc,tr_v v)
| LL (loc1,loc2) -> LL(loc1,loc2)
| FF (p,x,ft) -> FF (p,Misc.map_opt tr_v x,ft)
let tr_cond c = ConstrGen.map_constr tr_atom c
let parse s =
try
let lxb = Lexing.from_string s in
let c = StateParser.skip_loc_constr SL.token lxb in
Some (tr_cond c)
with
| Parsing.Parse_error
| LexMisc.Error _ -> None
module type DumpConfig = sig
val hexa : bool
val tr : string -> string
end
module Dump(O:DumpConfig) = struct
let pp_loc loc =
let s = MiscParser.dump_location loc in
O.tr s
let pp_atom a = match a with
| LV (rl,v) ->
sprintf "%s=%s" (dump_rloc pp_loc rl) (ToolsConstant.pp_norm O.hexa v)
| LL (l1,l2) ->
sprintf "%s=%s" (pp_loc l1) (pp_loc l2)
| FF f ->
Fault.pp_fatom ToolsConstant.pp_v (fun x -> x) f
let dump_prop chan = ConstrGen.dump_prop pp_atom chan
let dump chan = ConstrGen.dump_constraints chan pp_atom
end
module LocSet = MiscParser.LocSet
let get_locs_atom a =
match a with
| LV (loc,_) -> LocSet.add (loc_of_rloc loc)
| LL (loc1,loc2) ->
(fun k -> LocSet.add loc1 (LocSet.add loc2 k))
| FF (_,Some x,_) -> LocSet.add (MiscParser.Location_global x)
| FF (_,None,_) -> Misc.identity
let get_locs c = fold_constr get_locs_atom c LocSet.empty
let parse_observed s =
try
let lxb = Lexing.from_string s in
let locs,c = StateParser.main_loc_constr SL.token lxb in
Some
(LocSet.union
(LocationsItem.fold_locs LocSet.add locs LocSet.empty)
(get_locs c))
with
| Parsing.Parse_error
| LexMisc.Error _ -> None
let parse_locs_cond lxb =
try
let locs,c = StateParser.main_loc_constr SL.token lxb in
Some (locs,tr_cond c)
with
| Parsing.Parse_error
| LexMisc.Error _ -> None
let parse_locs s = parse_observed s (* Why a second fuction ? *)
let parse_filter lxb =
try
match StateParser.main_filter SL.token lxb with
| None -> None
| Some p -> Some (ConstrGen.map_prop tr_atom p)
with
| Parsing.Parse_error
| LexMisc.Error _ -> None
(* Code duplication? (with constraints) oh well! *)
module type I = sig
type v = ToolsConstant.v
type state
val state_mem : state -> MiscParser.location ConstrGen.rloc -> v -> bool
val state_eqloc : state -> MiscParser.location -> MiscParser.location -> bool
val state_fault : state -> (v,MiscParser.fault_type) Fault.atom -> bool
end
module Make(I:I) : sig
type state = I.state
type prop = (MiscParser.location, I.v, MiscParser.fault_type) ConstrGen.prop
type constr = prop ConstrGen.constr
(* check proposition *)
val check_prop : prop -> state -> bool
(* validation *)
val validate : constr -> state list -> bool
(* Return witness of interest / total number of outcomes *)
val witness : constr -> (state * Int64.t) list -> Int64.t * Int64.t
end =
struct
type state = I.state
type prop = (MiscParser.location, I.v,MiscParser.fault_type) ConstrGen.prop
type constr = prop ConstrGen.constr
let rec check_prop p state = match p with
| Atom (LV (x,v)) -> I.state_mem state x v
| Atom (LL (l1,l2)) -> I.state_eqloc state l1 l2
| Atom (FF f) -> I.state_fault state f
| Not p -> not (check_prop p state)
| And ps -> List.for_all (fun p -> check_prop p state) ps
| Or ps -> List.exists (fun p -> check_prop p state) ps
| Implies (p1, p2) ->
if check_prop p1 state then check_prop p2 state else true
let check_constr c states = match c with
| ForallStates p -> List.for_all (fun s -> check_prop p s) states
| ExistsState p -> List.exists (fun s -> check_prop p s) states
| NotExistsState p ->
not (List.exists (fun s -> check_prop p s) states)
let validate = check_constr
let witness c states =
let p = ConstrGen.prop_of c in
let pos,neg =
List.fold_left
(fun (pos,neg) (st,c) ->
if check_prop p st then
Int64.add c pos, neg
else
pos,Int64.add c neg)
(Int64.zero,Int64.zero) states in
match c with
| ExistsState _
| ForallStates _
->
pos,neg
| NotExistsState _ ->
neg,pos
end
|
