diff options
Diffstat (limited to 'abstract/relational_apron.ml')
| -rw-r--r-- | abstract/relational_apron.ml | 91 |
1 files changed, 85 insertions, 6 deletions
diff --git a/abstract/relational_apron.ml b/abstract/relational_apron.ml index bd078cf..926d2a9 100644 --- a/abstract/relational_apron.ml +++ b/abstract/relational_apron.ml @@ -1,3 +1,4 @@ +open Abstract_syntax_tree open Apron open Util open Environment_domain @@ -11,19 +12,86 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct (* abstract elements *) type t = man Abstract1.t + (* translation in trees *) + let rec texpr_of_expr e = + match fst e with + | AST_identifier (id, _) -> Texpr1.Var (Var.of_string id) + | AST_int_const (s, _) -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_string s)) + | AST_int_rand ((s, _), (t, _)) -> + Texpr1.Cst (Coeff.i_of_mpqf (Mpqf.of_string s) (Mpqf.of_string t)) + | AST_unary(AST_UNARY_PLUS, e) -> + texpr_of_expr e + | AST_unary(AST_UNARY_MINUS, e) -> + (* + (* APRON bug ? Unary negate seems to not work correctly... *) + Texpr1.Unop( + Texpr1.Neg, + (texpr_of_expr e), + Texpr1.Int, + Texpr1.Zero) + *) + Texpr1.Binop( + Texpr1.Sub, + Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")), + (texpr_of_expr e), + Texpr1.Int, + Texpr1.Zero) + | AST_binary( op, e1, e2) -> + let f = match op with + | AST_PLUS -> Texpr1.Add + | AST_MINUS -> Texpr1.Sub + | AST_MULTIPLY -> Texpr1.Mul + | AST_DIVIDE -> Texpr1.Div + | AST_MODULO -> Texpr1.Mod + | _ -> assert false + in + Texpr1.Binop + (f, (texpr_of_expr e1), (texpr_of_expr e2), Texpr1.Int, Texpr1.Zero) + | _ -> assert false + (* implementation *) let init = Abstract1.top manager (Environment.make [||] [||]) let bottom = Abstract1.bottom manager (Environment.make [||] [||]) let is_bot = Abstract1.is_bottom manager - let addvar x id = x (* TODO *) - let rmvar x id = x (* TODO *) + let addvar x id = + let env = Abstract1.env x in + let env2 = Environment.add env [| Var.of_string id |] [||] in + Abstract1.change_environment manager x env2 false + let rmvar x id = + let env = Abstract1.env x in + let env2 = Environment.remove env [| Var.of_string id |] in + Abstract1.change_environment manager x env2 false let vars x = List.map Var.to_string @@ - Array.to_list @@ snd @@ Environment.vars @@ Abstract1.env x + Array.to_list @@ fst @@ Environment.vars @@ Abstract1.env x - let assign x id e = x (* TODO *) - let compare x e1 e2 = x (* TODO *) + let assign x id e = + let expr = Texpr1.of_expr (Abstract1.env x) (texpr_of_expr e) in + let x' = + Abstract1.assign_texpr manager x + (Var.of_string id) expr None + in + if false then begin + Format.eprintf "Assign : "; + Abstract1.print Format.err_formatter x; + Format.eprintf " ; %s <- " id; + Texpr1.print Format.err_formatter expr; + Format.eprintf " ; "; + Abstract1.print Format.err_formatter x'; + Format.eprintf "@."; + end; + x' + let compare op x e1 e2 = + let env = Abstract1.env x in + let expr = Texpr1.Binop + (Texpr1.Sub, texpr_of_expr e2, texpr_of_expr e1, Texpr1.Int, Texpr1.Zero) in + let cons = Tcons1.make (Texpr1.of_expr env expr) op in + let ar = Tcons1.array_make env 1 in + Tcons1.array_set ar 0 cons; + Abstract1.meet_tcons_array manager x ar + let compare_leq = compare Tcons1.SUPEQ + let compare_eq = compare Tcons1.EQ let join = Abstract1.join manager let meet = Abstract1.meet manager @@ -31,7 +99,18 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct let subset = Abstract1.is_leq manager - let var_str x idl = "" (* TODO *) + let var_str x idl = + let prevars = vars x in + let rm_vars_l = List.filter (fun id -> not (List.mem id idl)) prevars in + (* print_list "prevars" prevars; + print_list "idl" idl; + print_list "rm_vars_l" rm_vars_l; *) + let rm_vars = Array.of_list (List.map Var.of_string rm_vars_l) in + let xx = Abstract1.forget_array manager x rm_vars false in + let b = Buffer.create 80 in + let s = Format.formatter_of_buffer b in + Abstract1.print s xx; Format.fprintf s "@?"; + (Buffer.contents b) end |