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
|
open Ast
open Num_domain
open Nonrelational
open Apron_domain
open Abs_interp
module Interpret = Interpret.I
module ItvND = Nonrelational.ND(Intervals_domain.VD)
module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND)
module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
(* command line options *)
let dump = ref false
let dumprn = ref false
let test = ref false
let vtest = ref false
let ai_itv = ref false
let ai_rel = ref false
let ai_itv_edd = ref false
let ai_root = ref "test"
let ai_widen_delay = ref 3
let ai_no_time_scopes = ref ""
let ai_init_scopes = ref ""
let ai_disj_v = ref ""
let ai_vci = ref false
let ifile = ref ""
let usage = "usage: analyzer [options] file.scade"
let options = [
"--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-rel", Arg.Set ai_rel, "Do abstract analysis using Apron.";
"--ai-itv-edd", Arg.Set ai_itv_edd, "Do abstract analysis using intervals and EDD disjunction domain.";
"--ai-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)";
"--wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3).";
"--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 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 = File_parser.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_rel || !ai_itv_edd then begin
let comma_split = Str.split (Str.regexp ",") in
let select_f x =
if x = "all"
then (fun _ -> true)
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
} in
if !ai_itv then AI_Itv.do_prog opt rp;
if !ai_rel then AI_Rel.do_prog opt rp;
if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
end;
if !vtest then do_test_interpret prog true
else if !test then do_test_interpret prog false;
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@." (Ast_printer.string_of_extent loc))
l
|
