path: root/abstract/relational_apron.ml

open Abstract_syntax_tree
open Apron
open Util
open Environment_domain

module RelationalDomain : ENVIRONMENT_DOMAIN = struct

    (* manager *)
    type man = Polka.loose Polka.t
    let manager = Polka.manager_alloc_loose ()

    (* 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 =
        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 @@ fst @@ Environment.vars @@ Abstract1.env x

    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
    let widen = Abstract1.widening manager

    let subset = Abstract1.is_leq manager

    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