path: root/abstract/constant_domain.ml

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