(*
  Cours "Sémantique et Application à la Vérification de programmes"

  Antoine Miné 2015
  Marc Chevalier 2018
  Josselin Giet 2021
  Ecole normale supérieure, Paris, France / CNRS / INRIA
*)

(*
  Signature of abstract domains representing sets of integers
  (for instance: constants or intervals).
 *)

open Abstract_syntax_tree

module type VALUE_DOMAIN =
  sig

    (* type of abstract elements *)
    (* an element of type t abstracts a set of integers *)
    type t

    (* unrestricted value: [-oo,+oo] *)
    val top: t

    (* bottom value: empty set *)
    val bottom: t

    (* constant: {c} *)
    val const: Z.t -> t

    (* interval: [a,b] *)
    val rand: Z.t -> Z.t -> t


    (* unary operation *)
    val unary: t -> int_unary_op -> t

    (* binary operation *)
    val binary: t -> t -> int_binary_op -> t


    (* comparison *)
    (* [compare x y op] returns (x',y') where
       - x' abstracts the set of v  in x such that v op v' is true for some v' in y
       - y' abstracts the set of v' in y such that v op v' is true for some v  in x
       i.e., we filter the abstract values x and y knowing that the test is true

       a safe, but not precise implementation, would be:
       compare x y op = (x,y)
     *)
    val compare: t -> t -> compare_op -> (t * t)


    (* backards unary operation *)
    (* [bwd_unary x op r] return x':
       - x' abstracts the set of v in x such as op v is in r
       i.e., we fiter the abstract values x knowing the result r of applying
       the operation on x
     *)
    val bwd_unary: t -> int_unary_op -> t -> t

     (* backward binary operation *)
     (* [bwd_binary x y op r] returns (x',y') where
       - x' abstracts the set of v  in x such that v op v' is in r for some v' in y
       - y' abstracts the set of v' in y such that v op v' is in r for some v  in x
       i.e., we filter the abstract values x and y knowing that, after
       applying the operation op, the result is in r
      *)
    val bwd_binary: t -> t -> int_binary_op -> t -> (t * t)


    (* set-theoretic operations *)
    val join: t -> t -> t
    val meet: t -> t -> t

    (* widening *)
    val widen: t -> t -> t

    (* narrowing *)
    val narrow: t -> t -> t

    (* subset inclusion of concretizations *)
    val subset: t -> t -> bool

    (* check the emptiness of the concretization *)
    val is_bottom: t -> bool

    (* print abstract element *)
    val print: Format.formatter -> t -> unit

end

open Cfg
open Domain

module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct
	module VMap = VarMap
	type t = Bot | E of V.t VMap.t
	let init _ = E VMap.empty (* Nonpresent variables are 0 *)
	let bottom = Bot


	let print out env = match env with
		| Bot   -> Format.fprintf out "@[<h 0>Bot@]"
		| E map -> begin Format.fprintf out "@[<h 0>{";
				VMap.iter (fun varid val1 -> Format.fprintf out "%a : %a@ " Cfg_printer.print_var varid V.print val1) map;
			   Format.fprintf out "}@]"; end

	let rec compute e expr = match expr with
		| CFG_int_unary (uop, aux) -> V.unary (compute e aux) uop
		| CFG_int_binary (bop, aux1, aux2) -> V.binary (compute e aux1) (compute e aux2) bop
		| CFG_int_var v -> (try ( VMap.find v e )with Not_found -> V.const Z.zero)
		| CFG_int_const c -> V.const c
		| CFG_int_rand (c1, c2) -> V.rand c1 c2

	let assign env v expr = match env with
		| Bot -> Bot
		| E envmap -> E (VMap.add v (compute envmap expr) envmap)

	let join env1 env2 = match (env1, env2) with
		| Bot, x | x, Bot -> x
		| E map1, E map2 ->
			 E (VMap.merge (fun v val1 val2 -> match val1, val2 with
				| None, None   -> None
				| None, Some x | Some x, None -> Some (V.join x (V.const Z.zero))
				| Some x, Some y -> Some (V.join x y)) map1 map2)
	let meet env1 env2 = match(env1, env2) with
		| Bot, x | x, Bot -> Bot
		| E map1, E map2 ->
			E (VMap.merge (fun v val1 val2 -> match val1, val2 with
				| None, None   -> None
				| None, Some x | Some x, None -> Some (V.meet x (V.const Z.zero))
				| Some x, Some y -> Some (V.meet x y)) map1 map2)


	type hc4_tree = HC4_int_unary  of int_unary_op * hc4_tree * V.t
		      | HC4_int_binary of int_binary_op * hc4_tree * hc4_tree * V.t
		      | HC4_int_var    of var * V.t 
		      | HC4_int_const  of Z.t * V.t
		      | HC4_int_rand   of Z.t*Z.t * V.t

	let get_abst hc4 = (match hc4 with
		| HC4_int_unary (_,_,v) -> v
		| HC4_int_binary (_,_,_,v) -> v
		| HC4_int_var (_,v) -> v
		| HC4_int_const (_,v) -> v
		| HC4_int_rand (_,_,v) -> v)

	let rec build_HC4 iexp mapenv = match iexp with
		| CFG_int_unary (uop, iexp') -> let sub = build_HC4 iexp' mapenv in HC4_int_unary (uop, sub, (V.unary (get_abst sub) uop))
		| CFG_int_binary (bop, iexp1, iexp2) -> let sub1, sub2 = build_HC4 iexp1 mapenv, build_HC4 iexp2 mapenv in
							HC4_int_binary (bop,sub1,sub2,(V.binary (get_abst sub1) (get_abst sub2) bop))
		| CFG_int_var v -> let abst = (try( VMap.find v mapenv )with Not_found -> V.const Z.zero) in HC4_int_var (v, abst)
		| CFG_int_const z -> let abst = V.const z in HC4_int_const (z, abst)
		| CFG_int_rand (a, b) -> let abst = V.rand a b in HC4_int_rand (a,b,abst)

	let rec revise_HC4 tree mapenv newval = match tree with
		| HC4_int_unary (uop, sub, abst) -> revise_HC4 sub mapenv (V.bwd_unary (get_abst sub) uop (V.meet abst newval))
		| HC4_int_binary (bop, sub1, sub2, abst) -> let refined1, refined2 = V.bwd_binary (get_abst sub1) (get_abst sub2) bop (V.meet abst newval) in begin
							    (*Format.printf "bwd_binary \"%a%s%a = %a\" -> %a, %a@ "
								V.print (get_abst sub1)
								(Cfg_printer.string_of_int_binary_op bop)
								V.print (get_abst sub2)
								V.print (V.meet abst newval)
								V.print (refined1)
								V.print (refined2);*)
							    meet (revise_HC4 sub1 mapenv refined1) (revise_HC4 sub2 mapenv refined2) end
		| HC4_int_var (v, abst)   -> E (VMap.add v (V.meet abst newval) mapenv)
		| HC4_int_const (z,abst)  -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv
		| HC4_int_rand (a,b,abst) -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv

	let rec guard_noneg env boolexp = match boolexp with
		| CFG_bool_unary (_, _) -> failwith "We were supposed to remove negations !!"
		| CFG_bool_binary (AST_AND, exp1, exp2) -> meet (guard_noneg env exp1) (guard_noneg env exp2)
		| CFG_bool_binary (AST_OR, exp1, exp2)  -> join (guard_noneg env exp1) (guard_noneg env exp2)
		| CFG_bool_const (b) -> if b then env else Bot
		| CFG_bool_rand -> env
		| CFG_compare (cop, iexp1, iexp2) -> match env with
			| Bot -> Bot
			| E mapenv ->	let hc4_1, hc4_2 = build_HC4 iexp1 mapenv, build_HC4 iexp2 mapenv in
					let newval1, newval2 = V.compare (get_abst hc4_1) (get_abst hc4_2) cop in (
					(*Format.printf "Refined comparison %a%s%a as %a%s%a@ "
						V.print (get_abst hc4_1)
						(Cfg_printer.string_of_compare_op cop)
						V.print (get_abst hc4_2)
						V.print newval1
						(Cfg_printer.string_of_compare_op cop)
						V.print newval2;*)
					meet (revise_HC4 hc4_1 mapenv newval1) (revise_HC4 hc4_2 mapenv newval2) )

	let guard env boolexp = guard_noneg env (rm_negations boolexp)
	let widen env1 env2 = match (env1, env2) with
		| Bot, x | x, Bot -> x
		| E map1, E map2 ->
			E (VMap.merge (fun v val1 val2 -> match val1, val2 with
				| None, None   -> None
				| None, Some x | Some x, None -> Some (V.widen x (V.const Z.zero))
				| Some x, Some y -> Some (V.widen x y)) map1 map2)
	let narrow env1 env2 = match(env1, env2) with
		| Bot, x | x, Bot -> Bot
		| E map1, E map2 ->
			E (VMap.merge (fun v val1 val2 -> match val1, val2 with
				| None, None   -> None
				| None, Some x | Some x, None -> Some (V.narrow x (V.const Z.zero))
				| Some x, Some y -> Some (V.narrow x y)) map1 map2)
	let subset env1 env2 = match env1, env2 with
		| Bot, _ -> true
		| _, Bot -> false
		| E map1, E map2 -> let b1 = VMap.for_all (fun varid val1 -> match VMap.find_opt varid map2 with
							| None -> V.subset val1 (V.const Z.zero)
							| Some val2 -> V.subset val1 val2) map1 in
				    let b2 = VMap.for_all (fun varid val2 -> match VMap.find_opt varid map1 with
							| None -> V.subset (V.const Z.zero) val2
							| Some val1 -> V.subset val1 val2) map2 in
				    b1 && b2
	let is_bottom env = match env with
		| Bot -> true
		| E map -> VMap.exists (fun varid val1 -> V.is_bottom val1) map
end