RETAB, CLEANUP

4 files changed, 15 insertions, 182 deletions

diff --git a/abstract/_constant_domain.ml b/abstract/_constant_domain.ml
deleted file mode 100644
index 544d2e9..0000000
--- a/abstract/_constant_domain.ml
+++ /dev/null
@@ -1,153 +0,0 @@
-open Util
-open Abstract_syntax_tree
-
-module CD : Domain.S =
-  struct
-
-    exception DivideByZero
-    exception TypeError
-    exception Bot
-    exception NotImplemented
-
-    type tv =   (* type for a variable *)
-      | Top
-      | I of Z.t
-
-    type ts =   (* type for an environment *)
-      | Bot
-      | Nb of tv VarMap.t
-
-    let top_ts = Nb VarMap.empty
-
-    let ts_union a b =
-      begin match a, b with
-      | Bot, Bot -> Bot
-      | Nb a, Bot -> Nb a
-      | Bot, Nb b -> Nb b
-      | Nb a, Nb b ->
-        Nb
-          (VarMap.fold
-            (fun var value a ->
-              try match VarMap.find var a with
-                | Top -> a
-                | I x ->
-                  match value with
-                  | I y when y = x -> a
-                  | _ -> VarMap.add var Top a
-              with
-              | Not_found -> VarMap.add var value a)
-          b a)
-      end
-
-    (* must not raise exception *)
-    let ts_add_bool_constraint expr (s : ts) =
-      s (* TODO, not necessary... *)
-
-
-    (* only evaluates numerical statements, raises
-      TypeError when result is bool *)
-    let rec eval_abs expr (s : tv VarMap.t) =
-      match expr with
-      | AST_unary(op, (i, _)) ->
-        begin match eval_abs i s with
-        | Top -> Top
-        | I x ->
-          match op with
-          | AST_UNARY_PLUS -> I x
-          | AST_UNARY_MINUS -> I (Z.neg x)
-          | _ -> raise TypeError
-        end
-      | AST_binary(op, (a, _), (b, _)) ->
-        begin match eval_abs a s, eval_abs b s with
-        | I x, I  y ->
-          begin match op with
-          | AST_PLUS -> I (Z.add x y)
-          | AST_MINUS -> I (Z.sub x y)
-          | AST_MULTIPLY -> I (Z.mul x y)
-          | AST_DIVIDE ->
-            if y = Z.zero then raise DivideByZero;
-            I (Z.div x y)
-          | AST_MODULO ->
-            if y = Z.zero then raise DivideByZero;
-            I (Z.rem x y)
-          | _ -> raise TypeError
-          end
-        | _ -> Top
-        end
-      | AST_identifier(id, _) ->
-        begin
-          try VarMap.find id s
-          with _ -> Top
-        end 
-      | AST_int_const(s, _) ->
-        I (Z.of_string s)
-      | AST_bool_const(_) -> raise TypeError
-      | AST_int_rand _ -> Top
-      | _ -> raise NotImplemented (* extensions *)
-
-    (* returns true if the expression can evaluate to true
-      returns false if the expression always evaluates to false *)
-    let rec eval_bool_abs expr (s : tv VarMap.t) =
-      true (* TODO *)
-
-    (* must not raise exception *)
-    let rec interp_abs stat s =
-      begin match s with
-      | Bot -> Bot
-      | Nb vars ->
-        begin match stat with
-        | AST_block b ->
-          List.fold_left
-            (fun ss (st, _) -> interp_abs st ss)
-            s b
-        | AST_assign ((id, _), (exp, _)) ->
-          begin
-            try
-              let value = eval_abs exp vars in
-              Nb (VarMap.add id value vars)
-            with _ -> Bot
-          end
-        | AST_if ((cond, _), (tb, _), None) ->
-          ts_union (Nb vars)
-            (interp_abs tb
-              (ts_add_bool_constraint cond (Nb vars)))
-        | AST_if ((cond, l), (tb, _), Some (eb, _)) ->
-          ts_union
-            (interp_abs tb
-              (ts_add_bool_constraint cond (Nb vars)))
-            (interp_abs eb
-              (ts_add_bool_constraint 
-                  (AST_unary (AST_NOT, (cond, l)))
-                (Nb vars)))
-        | AST_while ((cond, _), (body, _)) ->
-          let f s =
-            ts_union
-              s
-              (ts_add_bool_constraint cond s)
-          in
-            fix f (Nb vars)
-        | AST_HALT -> Bot
-        | AST_assert (cond, _) ->
-          if eval_bool_abs cond vars
-            then Nb vars
-            else begin
-              print_string "Assert fail\n";
-              Bot
-            end
-        | AST_print items ->
-          List.iter
-            (fun (var, _) ->
-              print_string (var ^ " = ");
-              try
-                match VarMap.find var vars with
-                | Top -> print_string "T\n"
-                | I x -> print_string (Z.to_string x ^ "\n")
-              with _ -> print_string "T\n")
-            items;
-          Nb vars
-        | _ -> raise NotImplemented (* extensions *)
-        end
-      end
-
-  end
-
diff --git a/abstract/_domain.ml b/abstract/_domain.ml
deleted file mode 100644
index 643a6ec..0000000
--- a/abstract/_domain.ml
+++ /dev/null
@@ -1,14 +0,0 @@
-open Abstract_syntax_tree
-
-module type S =
-  sig
-    type tv
-    type ts
-
-    val top_ts : ts
-
-    val interp_abs : stat -> ts -> ts
-    
-  end
-
-
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index c599a76..2f9f378 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -4,18 +4,18 @@ open Util
 
 module Make (E : ENVIRONMENT_DOMAIN) = struct
 
-    let neg (e, l) =
-        (AST_unary(AST_NOT, (e, l))), l
+    let neg e =
+        (AST_unary(AST_NOT, e)), snd e
 
-    let binop op (e, l) e2 =
-        (AST_binary (op, (e,l), e2)), l
-    let m1 (e, l) =
-        binop AST_MINUS (e, l) (AST_int_const("1", l), l)
-    let p1 (e, l) =
-        binop AST_PLUS (e, l) (AST_int_const("1", l), l)
+    let binop op e e2 =
+        (AST_binary (op, e, e2)), snd e
+    let m1 e =
+        binop AST_MINUS e (AST_int_const("1", snd e), snd e)
+    let p1 e =
+        binop AST_PLUS e (AST_int_const("1", snd e), snd e)
 
-    let bottom_with_vars =
-        List.fold_left E.addvar E.bottom
+    let bottom_with_vars vlist =
+        List.fold_left E.addvar E.bottom vlist
 
     let rec condition cond env =
         begin match fst cond with
@@ -29,7 +29,7 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
             E.join (condition e1 env) (condition e2 env)
 
         (* transformations : remove not *)
-        | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) ->
+        | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), _)) ->
             condition cond env
         | AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) ->
             condition
@@ -38,7 +38,7 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
             condition
                 (AST_binary(AST_AND, neg e1, neg e2), x) env
 
-        | AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) ->
+        | AST_unary (AST_NOT, (AST_binary(op, e1, e2), _)) ->
             let op2 = match op with
             | AST_LESS_EQUAL -> AST_GREATER
             | AST_LESS -> AST_GREATER_EQUAL
@@ -88,8 +88,8 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
                 (interp_stmt (condition cond env) tb)
                 (condition (neg cond) env)
         | AST_if (cond, tb, Some eb) ->
-            let e1 = (interp_stmt (condition cond env) tb) in
-            let e2 = (interp_stmt (condition (neg cond) env) eb) in
+            let e1 = interp_stmt (condition cond env) tb in
+            let e2 = interp_stmt (condition (neg cond) env) eb in
             E.join e1 e2
         | AST_while (cond, body) ->
             (* loop unrolling *)
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 39095b0..aa34d14 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -82,7 +82,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
                 | _ ->
                     let v1, v2 = eval env e1, eval env e2 in
                     let v1', v2' = f v1 v2 in
-                    if V.bottom = v1' ||V.bottom = v2'
+                    if V.bottom = v1' || V.bottom = v2'
                         then Bot
                         else Env env)
             x