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
|
open Formula
open Ast
open Util
open Environment_domain
open Apron
module D : ENVIRONMENT_DOMAIN = struct
(* manager *)
type man = Polka.loose Polka.t
let manager = Polka.manager_alloc_loose ()
type itv = Interval.t
(* abstract elements *)
type t = man Abstract1.t
(* direct translation of numerical expressions into Apron tree expressions *)
(* TODO : some variables have type real and not int... *)
let rec texpr_of_nexpr = function
| NIdent id -> Texpr1.Var (Var.of_string id)
| NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i))
| NRealConst r -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_float r))
| NUnary(AST_UPLUS, e) ->
texpr_of_nexpr e
| NUnary(AST_UMINUS, e) ->
(* APRON bug ? Unary negate seems to not work correctly... *)
Texpr1.Binop(
Texpr1.Sub,
Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")),
(texpr_of_nexpr e),
Texpr1.Int,
Texpr1.Zero)
| NBinary(op, e1, e2) ->
let f = match op with
| AST_PLUS -> Texpr1.Add
| AST_MINUS -> Texpr1.Sub
| AST_MUL -> Texpr1.Mul
| AST_DIV -> Texpr1.Div
| AST_MOD -> Texpr1.Mod
in
Texpr1.Binop(
f,
(texpr_of_nexpr e1),
(texpr_of_nexpr e2),
Texpr1.Int,
Texpr1.Zero)
(* direct translation of constraints into Apron constraints *)
let tcons_of_cons env (eq, op) =
let op = match op with
| CONS_EQ -> Tcons1.EQ
| CONS_NE -> Tcons1.DISEQ
| CONS_GT -> Tcons1.SUP
| CONS_GE -> Tcons1.SUPEQ
in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op
(* 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 isfloat =
let env = Abstract1.env x in
let env2 = if isfloat then
Environment.add env [||] [| Var.of_string id |]
else
Environment.add env [| Var.of_string id |] [||]
in
Abstract1.change_environment manager x env2 false
let forgetvar x id =
let v = [| Var.of_string id |] in
Abstract1.forget_array manager x v 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 =
let (ivt, fvt) = Environment.vars (Abstract1.env x) in
let ivl = List.map Var.to_string (Array.to_list ivt) in
let fvl = List.map Var.to_string (Array.to_list fvt) in
(List.map (fun x -> x, false) ivl) @ (List.map (fun x -> x, true) fvl)
let vbottom x =
Abstract1.bottom manager (Abstract1.env x)
let var_itv x id =
Abstract1.bound_variable manager x (Var.of_string id)
(* Apply some formula to the environment *)
let rec apply_cl x (cons, rest) =
let env = Abstract1.env x in
let tca = Array.of_list (List.map (tcons_of_cons env) cons) in
let ar = Tcons1.array_make env (Array.length tca) in
Array.iteri (Tcons1.array_set ar) tca;
let y = Abstract1.meet_tcons_array manager x ar in
apply_cl_r y rest
and apply_cl_r x = function
| CLTrue -> x
| CLFalse -> vbottom x
| CLAnd(a, b) ->
let y = apply_cl_r x a in
apply_cl_r y b
| CLOr(a, b) ->
let y = apply_cl x a in
let z = apply_cl x b in
Abstract1.join manager y z
let apply_f x f = apply_cl x (conslist_of_f f)
let assign x eqs =
let env = Abstract1.env x in
let vars = Array.of_list
(List.map (fun (id, _) -> Var.of_string id) eqs) in
let vals = Array.of_list
(List.map (fun (_, v) -> Texpr1.of_expr env (texpr_of_nexpr v)) eqs) in
Abstract1.assign_texpr_array manager x vars vals None
(* Ensemblistic operations *)
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
(* Pretty-printing *)
let print_all fmt x =
Abstract1.print fmt x;
Format.fprintf fmt "@?"
let print_vars fmt 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 (fun (id, _) -> Var.of_string id) rm_vars_l) in
let xx = Abstract1.forget_array manager x rm_vars false in
print_all fmt xx
let print_itv = Interval.print
end
|
