(*
  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
*)

open Cfg
open Iterable

let pp_asserts out a = 
	ArcSet.iter (fun arc -> match arc.arc_inst with
			| CFG_assert (b, ext) ->  Format.fprintf out "%a@ " Errors.pp_err (AssertFalse, ext, b)
			| _ -> failwith "Failed on non-assert") a


module Iterator (I : ITERABLE) = struct

	(*let pp_nodes out (s,nodelist) = 
		List.iter (fun node -> (Format.fprintf out "<%i>: %a@ " node.node_id D.print (node_abst node s))) nodelist
	*)
	let iterate cfg =
		let failed_asserts = ref ArcSet.empty in
		
		let rec do_fun (f : func) (ctx : I.t) = (*returns an abstraction of the result of exec*)
			let func_state = ref NodeMap.empty in (*avoid losing precision between function calls*)
			let func_dirty = ref NodeSet.empty in begin
			func_state := NodeMap.add f.func_entry ctx (!func_state);

			let node_abst n = try( NodeMap.find n !func_state )with Not_found -> I.bottom in
			
			let rec iterate n = begin
				(*Format.printf "@[<h 0> Handling node %i@]@ " n.node_id;*)
				func_dirty := NodeSet.remove n !func_dirty;
				let curr_abst = node_abst n in
				List.iter (fun arc ->
						let nv = I.do_compute arc curr_abst
								(fun a -> failed_asserts := ArcSet.add a !failed_asserts)
								do_fun in
						let s,b = I.accumulate arc (node_abst arc.arc_dst) nv in
						func_state := NodeMap.add arc.arc_dst s !func_state;
						if b then func_dirty := NodeSet.add arc.arc_dst !func_dirty;) n.node_out;
				if NodeSet.is_empty !func_dirty then () else
					iterate (NodeSet.choose !func_dirty)
				end in
			iterate f.func_entry;
			node_abst f.func_exit;
			end
		in
		begin
			Format.printf "@[<v 0>";
			let init_st = do_fun {func_id = -1; func_name = "_init";
					func_pos = Lexing.dummy_pos, Lexing.dummy_pos;
					func_entry = cfg.cfg_init_entry;
					func_exit = cfg.cfg_init_exit;
					func_args = [];
					func_ret = None;
					func_calls = []} I.init in
			let rec do_main l = match l with
				| x::_ when x.func_name = "main" -> do_fun x init_st
				| _::q -> do_main q
				| [] -> failwith "function main() not found" in
			let _ = do_main cfg.cfg_funcs in
			Format.printf "@]";
			!failed_asserts
		end
end

open Interval
open Sign
open Constant
open Naked
open Value_domain
open Congruence
open Reduced_product

module IntervalxCongr : CROSS_REDUCTION = struct
	module V = AddTopBot(Interval)
	module W = AddTopBot(Congruence)
	let cr (v,w) = match v,w with
		| _, W.Bot | V.Bot, _ -> V.Bot, W.Bot
		| V.Top, _ | _, W.Top -> v,w
		| V.V i, W.V c -> match c.multiple with
			| m when Z.equal Z.zero m -> if Z.leq i.lower c.offset && Z.leq c.offset i.upper then
					V.V {lower=c.offset; upper=c.offset}, w
				    else
					V.Bot, W.Bot
			| m -> (* Non-trivial multiplier : can only hope refining the bounds *)
				let q  = Z.div (Z.sub i.upper c.offset) m in (*rounds towards zero*)
				let q' = Z.div (Z.sub i.lower c.offset) m in
				if Z.equal q' q then
					let z = Z.add c.offset (Z.mul q' m) in
					let newint = V.const z and
					    newmod = W.const z in newint, newmod
				else (if Z.leq q' q then
					let newint = V.rand (Z.add c.offset (Z.mul q' m))
							(Z.add c.offset (Z.mul q m)) in
					newint, w
				else
					V.Bot, W.Bot)
				
end

module ConstIterator = Iterator(SimpleIterable(NonRelational(AddTopBot(Constants))))
module SignIterator  = Iterator(SimpleIterable(NonRelational(AddTopBot(Signs))))
module IntervalIterator  = Iterator(SimpleIterable(NonRelational(AddTopBot(Interval))))
module CongIterator = Iterator(SimpleIterable(NonRelational(AddTopBot(Congruence))))
module RPIterator  = Iterator(SimpleIterable(NonRelational(ReducedProduct(IntervalxCongr))))

module ConstDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Constants))))
module SignDisjIterator  = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Signs))))
module IntervalDisjIterator  = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Interval))))
module CongDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Congruence))))
module RPDisjIterator  = Iterator(DisjunctiveIterable(NonRelational(ReducedProduct(IntervalxCongr))))