summaryrefslogtreecommitdiff
path: root/abstract/apron_domain.ml
blob: d13afd787d8a55460118eb9185268cbab505169d (plain) (blame)
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