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
|
open Abstract_syntax_tree
open Apron
open Util
open Environment_domain
module RelationalDomain : ENVIRONMENT_DOMAIN = struct
(* manager *)
type man = Polka.loose Polka.t
let manager = Polka.manager_alloc_loose ()
(* abstract elements *)
type t = man Abstract1.t
(* translation in trees *)
let rec texpr_of_expr e =
match fst e with
| AST_identifier (id, _) -> Texpr1.Var (Var.of_string id)
| AST_int_const (s, _) -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_string s))
| AST_int_rand ((s, _), (t, _)) ->
Texpr1.Cst (Coeff.i_of_mpqf (Mpqf.of_string s) (Mpqf.of_string t))
| AST_unary(AST_UNARY_PLUS, e) ->
texpr_of_expr e
| AST_unary(AST_UNARY_MINUS, e) ->
(*
(* APRON bug ? Unary negate seems to not work correctly... *)
Texpr1.Unop(
Texpr1.Neg,
(texpr_of_expr e),
Texpr1.Int,
Texpr1.Zero)
*)
Texpr1.Binop(
Texpr1.Sub,
Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")),
(texpr_of_expr e),
Texpr1.Int,
Texpr1.Zero)
| AST_binary( op, e1, e2) ->
let f = match op with
| AST_PLUS -> Texpr1.Add
| AST_MINUS -> Texpr1.Sub
| AST_MULTIPLY -> Texpr1.Mul
| AST_DIVIDE -> Texpr1.Div
| AST_MODULO -> Texpr1.Mod
| _ -> assert false
in
Texpr1.Binop
(f, (texpr_of_expr e1), (texpr_of_expr e2), Texpr1.Int, Texpr1.Zero)
| _ -> assert false
(* implementation *)
let init = Abstract1.top manager (Environment.make [||] [||])
let bottom = Abstract1.bottom manager (Environment.make [||] [||])
let is_bot = Abstract1.is_bottom manager
let addvar x id =
let env = Abstract1.env x in
let env2 = Environment.add env [| Var.of_string id |] [||] in
Abstract1.change_environment manager x env2 false
let rmvar x id =
let v = [| Var.of_string id |] in
let env = Abstract1.env x in
let env2 = Environment.remove env v in
let y = Abstract1.forget_array manager x v false in
Abstract1.change_environment manager y env2 false
let vars x =
List.map Var.to_string @@
Array.to_list @@ fst @@ Environment.vars @@ Abstract1.env x
let assign x id e =
let expr = Texpr1.of_expr (Abstract1.env x) (texpr_of_expr e) in
let x' =
Abstract1.assign_texpr manager x
(Var.of_string id) expr None
in
if false then begin
Format.eprintf "Assign : ";
Abstract1.print Format.err_formatter x;
Format.eprintf " ; %s <- " id;
Texpr1.print Format.err_formatter expr;
Format.eprintf " ; ";
Abstract1.print Format.err_formatter x';
Format.eprintf "@.";
end;
x'
let compare op x e1 e2 =
let env = Abstract1.env x in
let expr = Texpr1.Binop
(Texpr1.Sub, texpr_of_expr e2, texpr_of_expr e1, Texpr1.Int, Texpr1.Zero) in
let cons = Tcons1.make (Texpr1.of_expr env expr) op in
let ar = Tcons1.array_make env 1 in
Tcons1.array_set ar 0 cons;
Abstract1.meet_tcons_array manager x ar
let compare_leq = compare Tcons1.SUPEQ
let compare_eq = compare Tcons1.EQ
let join = Abstract1.join manager
let meet = Abstract1.meet manager
let widen = Abstract1.widening manager
let subset = Abstract1.is_leq manager
let eq = Abstract1.is_eq manager
let var_str x idl =
let prevars = vars x in
let rm_vars_l = List.filter (fun id -> not (List.mem id idl)) prevars in
let rm_vars = Array.of_list (List.map Var.of_string rm_vars_l) in
let xx = Abstract1.forget_array manager x rm_vars false in
let b = Buffer.create 80 in
let s = Format.formatter_of_buffer b in
Abstract1.print s xx; Format.fprintf s "@?";
(Buffer.contents b)
end
|
