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
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
|
open Lexing
open Cmdline
open Ast
open Num_domain
open Nonrelational
open Apron_domain
open Enum_domain_edd
open Abs_interp_dynpart
module Interpret = Interpret.I
module ItvND = Apron_domain.ND_Box (* Nonrelational.ND(Intervals_domain.VD) *)
module PolyND = Apron_domain.ND_Poly
module OctND = Apron_domain.ND_Oct
module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
module AI_Poly = Abs_interp.I(Enum_domain.MultiValuation)(PolyND)
module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(OctND)
module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
module AI_Poly_EDD = Abs_interp_edd.I(PolyND)
module AI_Oct_EDD = Abs_interp_edd.I(OctND)
module AI_S_Itv_DP = Abs_interp_dynpart.I
(Enum_domain.MultiValuation)(ItvND)
module AI_S_Rel_DP = Abs_interp_dynpart.I
(Enum_domain.MultiValuation)(PolyND)
module AI_EDD_Itv_DP = Abs_interp_dynpart.I
(Enum_domain_edd.EDD)(ItvND)
module AI_EDD_Rel_DP = Abs_interp_dynpart.I
(Enum_domain_edd.EDD)(PolyND)
(* command line options *)
let times = ref false
let dump = ref false
let dumprn = ref false
let test = ref false
let vtest = ref false
let ai_itv = ref false
let ai_poly = ref false
let ai_oct = ref false
let ai_itv_edd = ref false
let ai_poly_edd = ref false
let ai_oct_edd = ref false
let ai_s_itv_dp = ref false
let ai_s_rel_dp = ref false
let ai_edd_itv_dp = ref false
let ai_edd_rel_dp = ref false
let ai_root = ref "test"
let ai_widen_delay = ref 5
let ai_no_time_scopes = ref "all"
let ai_init_scopes = ref "all"
let ai_disj_v = ref ""
let ai_max_dp_depth = ref 10
let ai_max_dp_width = ref 100
let ai_vci = ref false
let ai_vvci = ref false
let ifile = ref ""
let usage = "usage: analyzer [options] file.scade"
let options = [
"--exec-times", Arg.Set times,
"Show time spent in each function of the analyzer, for some functions";
"--dump", Arg.Set dump, "Dump program source.";
"--dump-rn", Arg.Set dumprn, "Dump program source, after renaming.";
"--vtest", Arg.Set vtest, "Verbose testing (direct interpret).";
"--test", Arg.Set test, "Simple testing (direct interpret).";
"--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals.";
"--ai-poly", Arg.Set ai_poly, "Do abstract analysis using Apron polyhedra domain.";
"--ai-oct", Arg.Set ai_oct, "Do abstract analysis using Apron octagon domain.";
"--ai-itv-edd", Arg.Set ai_itv_edd,
"Do abstract analysis using intervals and EDD disjunction domain.";
"--ai-poly-edd", Arg.Set ai_poly_edd,
"Do abstract analysis using Apron polyhedra domain and EDD disjunction domain.";
"--ai-oct-edd", Arg.Set ai_oct_edd,
"Do abstract analysis using Apron octagon domain and EDD disjunction domain.";
"--ai-s-itv-dp", Arg.Set ai_s_itv_dp,
"Do abstract analysis using dynamic partitionning method, "^
"with intervals and valuation domain for enums.";
"--ai-s-rel-dp", Arg.Set ai_s_rel_dp,
"Do abstract analysis using dynamic partitionning method, "^
"with Apron and valuation domain for enums.";
"--ai-edd-itv-dp", Arg.Set ai_edd_itv_dp,
"Do abstract analysis using dynamic partitionning method, "^
"with intervals and EDD domain for enums.";
"--ai-edd-rel-dp", Arg.Set ai_edd_rel_dp,
"Do abstract analysis using dynamic partitionning method, "^
"with Apron and EDD domain for enums.";
"--ai-vci", Arg.Set ai_vci,
"Verbose chaotic iterations (show state at each iteration)";
"--ai-vvci", Arg.Set ai_vvci,
"Very verbose chaotic iterations (show everything all the time)";
"--ai-wd", Arg.Set_int ai_widen_delay,
"Widening delay in abstract analysis of loops (default: 3).";
"--ai-max-dp-depth", Arg.Set_int ai_max_dp_depth,
"Maximum depth in the dynamic partitionning tree.";
"--ai-max-dp-width", Arg.Set_int ai_max_dp_width,
"Maximum number of dynamically partitionned locations.";
"--root", Arg.Set_string ai_root,
"Root node for abstract analysis (default: test).";
"--no-time", Arg.Set_string ai_no_time_scopes,
"Scopes for which not to introduce a 'time' variable in analysis.";
"--disj", Arg.Set_string ai_disj_v,
"Variables for which to introduce a disjunction.";
"--init", Arg.Set_string ai_init_scopes,
"Scopes for which to introduce a 'init' variable in analysis.";
]
let parse_file (filename : string) : prog =
let f = open_in filename in
let lex = from_channel f in
try
lex.lex_curr_p <- { lex.lex_curr_p with pos_fname = filename; };
Parser.file Lexer.token lex
with
| Parser.Error ->
Util.error (Printf.sprintf "Parse error (invalid syntax) near %s"
(Util.string_of_position lex.lex_start_p))
| Failure "lexing: empty token" ->
Util.error (Printf.sprintf "Parse error (invalid token) near %s"
(Util.string_of_position lex.lex_start_p))
let do_test_interpret prog verbose =
let f0 _ = false in
let s0 = Interpret.init_state (Typing.root_prog prog "test" f0 f0) in
if verbose then begin
Format.printf "Init state:@.";
Interpret.print_state Format.std_formatter s0;
end;
let rec it i st =
let next_st, out =
Interpret.step st
["i", Interpret.int_value i]
in
if verbose then begin
Format.printf "@.> Step %d:@." i;
Interpret.print_state Format.std_formatter st;
Format.printf "Outputs:@.";
List.iter
(fun (k, v) -> Format.printf "%s = %s@."
k (Interpret.str_repr_of_val v))
out;
end else begin
Format.printf "%d. %s %s %s@." i
(Interpret.str_repr_of_val (List.assoc "a" out))
(Interpret.str_repr_of_val (List.assoc "b" out))
(Interpret.str_repr_of_val (List.assoc "c" out));
end;
if not (Interpret.as_bool (List.assoc "exit" out)) then
it (i+1) next_st
in
it 0 s0
let () =
(* AI_Itv_EDD.test (); *)
Arg.parse options (fun f -> ifile := f) usage;
if !ifile = "" then begin
Format.eprintf "No input file...@.";
exit 1
end;
try
let prog = parse_file !ifile in
if !dump then Ast_printer.print_prog Format.std_formatter prog;
let prog = Rename.rename_prog prog in
if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
if !ai_itv || !ai_poly || !ai_oct
|| !ai_itv_edd || !ai_poly_edd || !ai_oct_edd
|| !ai_s_itv_dp || !ai_s_rel_dp
|| !ai_edd_itv_dp || !ai_edd_rel_dp then
begin
let comma_split = Str.split (Str.regexp ",") in
let select_f x =
if x = "all" then
(fun _ -> true)
else if x = "last" then
(fun i -> i.[0] = 'L')
else if String.length x > 5 && String.sub x 0 5 = "last+" then
let psl = comma_split
(String.sub x 5 (String.length x - 5)) in
(fun i -> i.[0] = 'L' || List.mem i psl)
else
(fun i -> List.mem i (comma_split x))
in
let rp = Typing.root_prog prog !ai_root
(select_f !ai_no_time_scopes)
(select_f !ai_init_scopes) in
let disj = select_f !ai_disj_v in
let opt = {
widen_delay = !ai_widen_delay;
disjunct = disj;
verbose_ci = !ai_vci;
vverbose_ci = !ai_vvci;
max_dp_width = !ai_max_dp_width;
max_dp_depth = !ai_max_dp_depth;
} in
if !ai_itv then AI_Itv.do_prog opt rp;
if !ai_poly then AI_Poly.do_prog opt rp;
if !ai_oct then AI_Oct.do_prog opt rp;
if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
if !ai_poly_edd then AI_Poly_EDD.do_prog opt rp;
if !ai_oct_edd then AI_Oct_EDD.do_prog opt rp;
if !ai_s_itv_dp then AI_S_Itv_DP.do_prog opt rp;
if !ai_s_rel_dp then AI_S_Rel_DP.do_prog opt rp;
if !ai_edd_itv_dp then AI_EDD_Itv_DP.do_prog opt rp;
if !ai_edd_rel_dp then AI_EDD_Rel_DP.do_prog opt rp;
end;
if !vtest then do_test_interpret prog true
else if !test then do_test_interpret prog false;
if !times then Util.show_times();
with
| Util.NoLocError e -> Format.eprintf "Error: %s@." e
| Util.LocError(l, e) ->
Format.eprintf "Error: %s@." e;
List.iter
(fun loc -> Format.eprintf "At: %s@." (Util.string_of_extent loc))
l
|
