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
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2012-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. *)
(****************************************************************************)
(*********************************************)
(* Project condition w.r.t. set of locations *)
(*********************************************)
open Printf
module type Config = sig
val verbose : int
val locs : MiscParser.LocSet.t TblRename.t
end
module Make(Config:Config) =
struct
module D = Splitter.Default
module LU = LexUtils.Make(D)
module S = Splitter.Make(D)
open ConstrGen
let check_locs name =
try Some (TblRename.find_value Config.locs name)
with Not_found -> None
let is_true = function
| And [] -> true
| _ -> false
let ors ps =
if List.exists is_true ps then And []
else Or ps
let ands ps =
let ps = List.filter (fun p -> not (is_true p)) ps in
And ps
let rec proj_p locs p = match p with
| Not _
| Implies _ -> Warn.fatal "Bad condition in mproj"
| Atom (LL (loc,_)|LV (Loc loc,_)) as p ->
if MiscParser.LocSet.mem loc locs then p else And []
| Atom (LV (Deref _,_)) ->
prerr_endline "TODO" ; assert false
| Atom (FF (_,None,_)) -> And []
| Atom (FF (_,Some x,_)) ->
let loc = MiscParser.Location_global (Constant.check_sym x) in
if MiscParser.LocSet.mem loc locs then p else And []
| Or ps ->
Or (List.map (proj_p locs) ps)
| And ps ->
ands (List.map (proj_p locs) ps)
let proj locs = function
| ForallStates p -> ForallStates (proj_p locs p)
| ExistsState p -> ExistsState (proj_p locs p)
| NotExistsState p -> NotExistsState (proj_p locs p)
module Dump =
LogConstr.Dump
(struct
let hexa = false
let tr = Misc.identity
end)
let from_chan chan fname in_chan =
try
let { Splitter.locs = locs; name=name; _} =
S.split fname in_chan in
let tname = name.Name.name in
match check_locs tname with
| None -> ()
| Some ls ->
let _,_,(constr_start,constr_end),(_last_start,_loc_eof) = locs in
let lexbuf = LU.from_section (constr_start,constr_end) in_chan in
match LogConstr.parse_locs_cond lexbuf with
| None -> ()
| Some (ls0,c0) ->
assert (ls0=[]) ;
let c = proj ls c0 in
fprintf chan "%s \"" tname ;
Dump.dump chan c ;
fprintf chan "\"\n" ;
()
with LexMisc.Error (msg,pos) ->
Printf.eprintf
"%a: Lex error %s (in %s)\n" Pos.pp_pos pos msg fname ;
raise Misc.Exit
let from_file chan name =
try
Misc.input_protect
(fun in_chan -> from_chan chan name in_chan)
name
with Misc.Exit -> ()
| Misc.Fatal msg|Misc.UserError msg ->
eprintf "Fatal error is not fatal, %s\n" msg
let from_args args = Misc.iter_argv (from_file stdout) args
end
(**********)
(* Driver *)
(**********)
let verbose = ref 0
let args = ref []
let locs = ref []
let opts =
[ "-v", Arg.Unit (fun () -> incr verbose)," be verbose";
"-locs", Arg.String (fun s -> locs := !locs @ [s]), " <name> specify location files";]
let prog =
if Array.length Sys.argv > 0 then Sys.argv.(0)
else "mproj"
let () =
Arg.parse opts
(fun a -> args := a :: !args)
(sprintf "Usage %s [options] [test]*" prog)
module Verbose = struct let verbose = !verbose end
module LR = LexRename.Make(Verbose)
module X =
Make
(struct
let verbose = !verbose
let locs = LR.read_from_files !locs LogConstr.parse_locs
end)
let () = X.from_args !args
|
