summaryrefslogtreecommitdiff
path: root/abstract/apron_domain.ml
blob: 45803fc51415547e197e73aa78523425b2a3df61 (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
open Formula
open Ast

open Util
open Num_domain

open Apron

module ND : NUMERICAL_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 v_env vars = 
        let intv = List.map
              (fun (s, _) -> Var.of_string s)
              (List.filter (fun (_, n) -> not n) vars) in
        let realv = List.map
              (fun (s, _) -> Var.of_string s)
              (List.filter (fun (_, n) -> n) vars) in
        (Environment.make (Array.of_list intv) (Array.of_list realv))

    let top vars =
      Abstract1.top manager (v_env vars)
    let bottom vars = Abstract1.bottom manager (v_env vars)
    let is_bot = Abstract1.is_bottom manager
    let is_top = Abstract1.is_top manager

    let forgetvar x id =
        let v = [| Var.of_string id |] in
        Abstract1.forget_array manager x v 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 project x id =
        Abstract1.bound_variable manager x (Var.of_string id)

    (* Apply some formula to the environment *)
    let apply_cl x cons =
        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;
        Abstract1.meet_tcons_array manager x ar

    let apply_cons x cons = apply_cl x [cons]


    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 fmt x =
        Abstract1.minimize manager 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 fmt xx

    let print_itv = Interval.print

end