summaryrefslogtreecommitdiff
path: root/abstract/nonrelational.ml
blob: b3129c0ecf241fc626c1932f8e25ed583ec5526a (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
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
open Formula
open Util
open Ast

open Value_domain
open Num_domain

let debug = false

(* Restricted domain, only support integers *)

module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
    type env = V.t VarMap.t

    type t = Env of env | Bot
    type itv = Value_domain.itv

    let top vars = Env
      (List.fold_left
          (fun e (v, _) -> VarMap.add v V.top e)
          VarMap.empty vars)
    let bottom _ = Bot

    let get_var env id =
        try VarMap.find id env
        with Not_found -> V.top
    
    (* utilities *)

    let rec eval env = function
        | NIdent id -> get_var env id
        | NIntConst i -> V.const i
        | NRealConst f -> V.const (int_of_float f) (* TODO floats *)
        | NUnary (AST_UPLUS, e) -> eval env e
        | NUnary (AST_UMINUS, e) -> V.neg (eval env e)
        | NBinary (op, e1, e2) ->
            let f = match op with
            | AST_PLUS -> V.add
            | AST_MINUS -> V.sub
            | AST_MUL -> V.mul
            | AST_DIV -> V.div
            | AST_MOD -> V.rem
            in f (eval env e1) (eval env e2)

    let strict env =                    (*      env -> t        *)
        if VarMap.exists (fun _ x -> x = V.bottom) env
            then Bot
            else Env env
    let strict_apply f = function       (* (env -> t) -> t -> t *)
        | Bot -> Bot
        | Env e -> match f e with
            | Bot -> Bot
            | Env e -> strict e

    (* implementation *)

    let is_bot env = match env with
        | Bot -> true
        | Env env -> strict env = Bot

    let forgetvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x

    let vars env = match env with
        | Bot -> []
        | Env env -> List.map (fun (k, _) -> (k, false)) (VarMap.bindings env)
    let vbottom _ = Bot

    let project x id = match x with
        | Bot -> Value_domain.Bot
        | Env env -> V.to_itv (get_var env id)

    (* Set-theoretic operations *)
    let f_in_merge f _ a b = match a, b with
      | Some a, None -> Some a
      | None, Some b -> Some b
      | Some a, Some b -> Some (f a b)
      | _ -> assert false

    let join a b = match a, b with
        | Bot, x | x, Bot -> x
        | Env m, Env n ->
            strict (VarMap.merge (f_in_merge V.join) m n)
    
    let meet a b = match a, b with
        | Bot, _ | _, Bot -> Bot
        | Env m, Env n ->
            strict (VarMap.merge (f_in_merge V.meet) m n)

    let widen a b = match a, b with
        | Bot, x | x, Bot -> x
        | Env m, Env n ->
            strict (VarMap.merge (f_in_merge V.widen) m n)

    (* Inclusion and equality *)
    let subset a b = match a, b with
        | Bot, x -> true
        | Env _, Bot -> false
        | Env m, Env n ->
            VarMap.for_all
                (fun id vn ->
                  try let vm = VarMap.find id m in V.subset vm vn
                  with Not_found -> vn = V.top)
                n

    let eq a b = match a, b with
        | Bot, Bot -> true
        | Env m, Env n ->
            VarMap.for_all2o
                (fun _ v -> v = V.top)
                (fun _ v -> v = V.top)
                (fun _ a b -> a = b)
                m n
        | _ -> false

    (* Apply some formula to the environment *)
    let apply_cons env (expr, sign) =
        let inv_op = function
          | AST_LT -> AST_GT
          | AST_GT -> AST_LT
          | AST_LE -> AST_GE
          | AST_GE -> AST_LE
          | x -> x
        in
        let rec extract_var (lhs, op, rhs) =
          match lhs with
          | NIdent i -> [i, op, rhs]
          | NIntConst _ | NRealConst _ -> []
          | NUnary(AST_UPLUS, x) -> extract_var (x, op, rhs)
          | NUnary(AST_UMINUS, x) ->
            extract_var (x, inv_op op, NUnary(AST_UMINUS, x))
          | NBinary(AST_PLUS, a, b) ->
            extract_var (a, op, NBinary(AST_MINUS, rhs, b)) @
            extract_var (b, op, NBinary(AST_MINUS, rhs, a))
          | NBinary(AST_MINUS, a, b) ->
            extract_var (a, op, NBinary(AST_PLUS, rhs, b)) @
            extract_var (b, inv_op op, NBinary(AST_MINUS, a, rhs))
          | NBinary(AST_MUL, a, b) ->
            extract_var (a, op, NBinary(AST_DIV, rhs, b)) @
            extract_var (b, op, NBinary(AST_DIV, rhs, a))
          | NBinary(AST_DIV, a, b) ->
            extract_var (a, op, NBinary(AST_MUL, rhs, b)) @
            extract_var (b, inv_op op, NBinary(AST_DIV, a, rhs))
          | NBinary(AST_MOD, _, _) -> []
        in
        let zop = match sign with
          | CONS_EQ -> AST_EQ | CONS_NE -> AST_NE
          | CONS_GT -> AST_GT | CONS_GE -> AST_GE
        in
        let restrict_var env (i, op, expr) =
          strict_apply (fun env ->
            let v1, v2 = get_var env i, eval env expr in
            let v1' = match op with
            | AST_EQ -> V.meet v1 v2
            | AST_NE -> v1
            | AST_LE -> let u, _ = V.leq v1 v2 in u
            | AST_GE -> let _, v = V.leq v2 v1 in v
            | AST_LT -> let u, _ = V.leq v1 (V.sub v2 (V.const 1)) in u
            | AST_GT -> let _, v = V.leq (V.add v2 (V.const 1)) v1 in v
            in
            if debug then Format.printf
              "restrict %s %s @[<hv>%a@] : %s %s -> %s@." i 
              (Formula_printer.string_of_binary_rel op)
              Formula_printer.print_num_expr expr
              (V.to_string v1) (V.to_string v2) (V.to_string v1');
            Env (VarMap.add i v1' env))
          env
        in
        List.fold_left restrict_var env
          (extract_var (expr, zop, NIntConst 0))

    let apply_cl x cl =
        let f x = List.fold_left apply_cons x cl in
        fix eq f x

    (* Assignment *)
    let assign x exprs =
        let aux env =
          let vars = List.map (fun (id, v) -> (id, eval env v)) exprs in
          let env2 =
            List.fold_left (fun e (id, v) -> VarMap.add id v e)
              env vars
          in Env env2
        in
        strict_apply aux x

        
    (* pretty-printing *)
    let print_vars fmt env ids =
        match env with
        | Bot -> Format.fprintf fmt "⊥"
        | Env env ->
            let l = List.map (fun id -> (get_var env id, id)) ids in
            let s = List.sort Pervasives.compare l in
            let rec bl = function
              | [] -> []
              | (v, id)::q when v <> V.top ->
                begin match bl q with
                | (vv, ids)::q when vv = v -> (v, id::ids)::q
                | r -> (v, [id])::r
                end
              | _::q -> bl q
            in
            let sbl = bl s in
            if sbl = [] then
              Format.fprintf fmt "⊤"
            else begin
              Format.fprintf fmt "@[<v 2>{ ";
              List.iteri
                (fun j (v, ids) ->
                  if j > 0 then Format.fprintf fmt "@ ";
                  Format.fprintf fmt "@[<hov 4>";
                  List.iteri
                    (fun i id ->
                      if i > 0 then Format.fprintf fmt ",@ ";
                      Format.fprintf fmt "%a" Formula_printer.print_id id)
                    ids;
                  match V.as_const v with
                  | Some i -> Format.fprintf fmt " = %d@]" i
                  | _ -> Format.fprintf fmt " ∊ %s@]" (V.to_string v))
                sbl;
              Format.fprintf fmt " }@]"
            end

    let print fmt x =
        print_vars fmt x (List.map fst (vars x))

    let print_itv fmt x =
        Format.fprintf fmt "%s" (string_of_itv x)
    
end