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
|
open Ast
open Num_domain
open Nonrelational
open Apron_domain
module Interpret = Interpret.I
module ItvND = Nonrelational.ND(Intervals_domain.VD)
module AI_Itv = Abs_interp.I(Enum_domain.Valuation)(ItvND)
module AI_Rel = Abs_interp.I(Enum_domain.Valuation)(Apron_domain.ND)
(* 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_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 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.";
"--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 () =
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 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
if !ai_itv then AI_Itv.do_prog !ai_widen_delay disj rp;
if !ai_rel then AI_Rel.do_prog !ai_widen_delay disj 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
|
