summaryrefslogtreecommitdiffstats
path: root/abstract/nonrelational.ml
blob: 6e2ff2b37efffded010236d53d6c54ce9d62e3f5 (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

open Abstract_syntax_tree
open Util

open Value_domain
open Environment_domain


module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
    type env = V.t VarMap.t

    type t = Env of env | Bot

    let init = Env VarMap.empty
    let bottom = Bot

    let get_var env id =
        try VarMap.find id env
        with Not_found -> V.top


    (* utilities *)

    let rec eval env expr =
        begin match fst expr with
        | AST_identifier (id, _) -> get_var env id
        | AST_int_const (s, _) -> V.const (Z.of_string s)
        | AST_int_rand ((s, _), (t, _)) -> V.rand (Z.of_string s) (Z.of_string t)
        | AST_unary (AST_UNARY_PLUS, e) -> eval env e
        | AST_unary (AST_UNARY_MINUS, e) -> V.neg (eval env e)
        | AST_unary (_, e) -> V.bottom
        | AST_binary (op, e1, e2) ->
            let f = match op with
            | AST_PLUS -> V.add
            | AST_MINUS -> V.sub
            | AST_MULTIPLY -> V.mul
            | AST_DIVIDE -> V.div
            | AST_MODULO -> V.rem
            | _ -> fun _ _ -> V.bottom
            in f (eval env e1) (eval env e2)
        | _ -> assert false (* unimplemented extension *)
        end

    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 addvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x
    let rmvar x id = strict_apply (fun y -> Env (VarMap.remove id y)) x

    let assign x id expr = strict_apply
        (fun env -> Env (VarMap.add id (eval env expr) env))
        x
    let compare x e1 e2 =
        strict_apply (fun env -> match fst e1, fst e2 with
                | AST_identifier(a, _), AST_identifier(b, _) ->
                    let v1, v2 = get_var env a, get_var env b in
                    let v1', v2' = V.leq v1 v2 in
                    Env (VarMap.add a v1' (VarMap.add b v1' env))
                | AST_identifier(a, _), AST_int_const(s, _) ->
                    let v1, v2 = get_var env a, V.const (Z.of_string s) in
                    let v1', _ = V.leq v1 v2 in
                    Env (VarMap.add a v1' env)
                | AST_int_const(s, _), AST_identifier(b, _) ->
                    let v1, v2 = V.const (Z.of_string s), get_var env b in
                    let _, v2' = V.leq v1 v2 in
                    Env (VarMap.add b v2' env)
                | _ -> Env env)
            x

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

    let widen a b = match a, b with
        | Bot, x | x, Bot -> x
        | Env m, Env n ->
            strict (VarMap.map2z (fun _ a b -> V.widen a b) m n)
    
    let subset a b = match a, b with
        | Bot, x -> true
        | Env _, Bot -> false
        | Env m, Env n ->
            VarMap.for_all2o
                (fun _ _ -> true)
                (fun _ _ -> true)
                (fun _ a b -> V.subset a b)
                m n
        
end