diff options
| -rw-r--r-- | abstract/constant_domain.ml | 5 | ||||
| -rw-r--r-- | abstract/environment_domain.ml | 5 | ||||
| -rw-r--r-- | abstract/interpret.ml | 29 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 26 | ||||
| -rw-r--r-- | abstract/value_domain.ml | 3 |
5 files changed, 61 insertions, 7 deletions
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml index 4bd5cf2..d142228 100644 --- a/abstract/constant_domain.ml +++ b/abstract/constant_domain.ml @@ -50,4 +50,9 @@ module Constants : VALUE_DOMAIN = struct then Int a, Int b else Bot, Bot | x, y -> x, y + + let to_string = function + | Bot -> "bot" + | Top -> "top" + | Int i -> "{" ^ (Z.to_string i) ^ "}" end diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml index f5614fe..254f755 100644 --- a/abstract/environment_domain.ml +++ b/abstract/environment_domain.ml @@ -6,6 +6,7 @@ module type ENVIRONMENT_DOMAIN = sig (* construction *) val init : t val bottom : t + val is_bot : t -> bool (* variable management *) val addvar : t -> id -> t @@ -22,6 +23,10 @@ module type ENVIRONMENT_DOMAIN = sig (* order *) val subset : t -> t -> bool + + (* pretty-printing *) + val var_str : t -> id list -> string + val all_vars_str : t -> string end diff --git a/abstract/interpret.ml b/abstract/interpret.ml index 51c7cd6..fe998a6 100644 --- a/abstract/interpret.ml +++ b/abstract/interpret.ml @@ -17,7 +17,14 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct E.meet (condition e1 env) (condition e2 env) | AST_binary (AST_OR, e1, e2) -> E.join (condition e1 env) (condition e2 env) - | _ -> env (* TODO : encode some transformations *) + (* transformations *) + | AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) -> + condition + (AST_binary(AST_OR, neg e1, neg e2), x) env + | AST_unary (AST_NOT, (AST_binary(AST_OR, e1, e2), x)) -> + condition + (AST_binary(AST_AND, neg e1, neg e2), x) env + | _ -> env (* TODO : encode some more transformations *) end let rec interp_stmt env stat = @@ -39,19 +46,31 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct env | AST_HALT -> E.bottom | AST_assert (cond, l) -> - (* TODO *) - env + if not + (E.is_bot (condition (neg (cond, l)) env)) + then begin + print_string (Abstract_syntax_printer.string_of_extent l); + print_string ": ERROR: assertion failure\n" + end; + condition (cond, l) env | AST_print items -> - (* TODO *) + print_string (Abstract_syntax_printer.string_of_extent (snd stat)); + print_string ": "; + print_string (E.var_str env (List.map fst items)); + print_string "\n"; env | _ -> assert false (* not implemented *) end let interpret prog = - List.fold_left + let result = List.fold_left (fun env x -> match x with | AST_stat st -> interp_stmt env st | _ -> env) E.init (fst prog) + in + print_string "Output: "; + print_string (E.all_vars_str result); + print_string "\n" end diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 6e2ff2b..d4118da 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -16,8 +16,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct let get_var env id = try VarMap.find id env with Not_found -> V.top - - + (* utilities *) let rec eval env expr = @@ -52,6 +51,10 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct (* implementation *) + let is_bot env = match env with + | Bot -> true + | Env env -> strict env = Bot + 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 @@ -100,4 +103,23 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct (fun _ a b -> V.subset a b) m n + (* pretty-printing *) + let var_str env vars = + match env with + | Bot -> "bot" + | Env env -> + let v = List.fold_left + (fun s id -> + (if s = "" then s else s ^ ", ") ^ + id ^ " in " ^ (V.to_string (get_var env id)) + ) + "" + vars + in + "[ " ^ v ^ " ]" + + let all_vars_str env = + match env with + | Bot -> "bot" + | Env map -> var_str env (List.map fst (VarMap.bindings map)) end diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml index a0f082f..9cf6d76 100644 --- a/abstract/value_domain.ml +++ b/abstract/value_domain.ml @@ -25,4 +25,7 @@ module type VALUE_DOMAIN = sig (* boolean test *) val leq : t -> t -> t * t (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *) + + (* pretty-printing *) + val to_string : t -> string end |