CristalCaveGem » LustreC

# z3 (optional)

# option to rely on github version if installed

AC_ARG_WITH(z3_github, [AS_HELP_STRING([--with-z3-github],

              [Rely on Z3 as distributed by the official github

	       repo rather then the opam distribution. Disabled by default.])])

AS_IF([test "x$with_z3_github" != "xyes"],

      [z3name=z3],

      [z3name=Z3]

      )

AC_MSG_CHECKING(z3 library)

#define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))

AS_IF([ocamlfind query $z3name >/dev/null 2>&1],

    [z3=yes; AC_MSG_RESULT([yes])],[seal=no; AC_MSG_RESULT(no)],

   AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package($z3name)")

   AS_IF([test "x$z3name" = "xZ3"],

   	       [define([Z3path], esyscmd([ocamlfind query Z3 | tr -d '\n']))

	        AC_SUBST(Z3LIBPATH, "Z3path")],

 	       [define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))

	        AC_SUBST(Z3LIBPATH, "z3path")]

		)

      dnl AC_MSG_WARN(It is currently located in "z3path")

<utils.*>                       : use_unix

<**/*.native>                   : package(yojson)

<tools/zustre/zustre_cex.*>                   : package(yojson)

    | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err

(* compile-command:"make -C ../.. lustrev" *)

(* Rebuilding Cex *)

(* In order to properly rebuild the Cex, one needsthe unsliced model. Otherwise

   some input or state variables are removed.

*)

open Lustre_types

open Machine_code_types

(* open Machine_code_common *)

open Zustre_common

let build_cex machine machines decl_err =

  (* Recovering associated top machine (to build full traces) and property *) 

  (* TODO: for example extract top node and ok prop. We may have multiple

     MAIN/ERR loaded at the same time. Each of them should be assocaited with a

     CEX/Inv/Timeout.*)

  let node_id = machine.mname.node_id in

  (* Original code used the function Z3.Fixedpoint.get_ground_sat_answer !fp *)

  let stats = Z3.Fixedpoint.get_statistics !fp in

  Format.eprintf "cex: %s@.%i conjuncts: @[<v 0>%a@]@."

    (Z3.Expr.to_string cex)

    (List.length conjuncts)

    (Utils.fprintf_list ~sep:"@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) conjuncts;

  (* Checking size *)

  let inputs = machine.mstep.step_inputs in

  let nb_inputs = List.length inputs in

  let outputs = machine.mstep.step_outputs in

  let nb_outputs = List.length inputs in

  let nb_mems = List.length (full_memory_vars machines machine) in

  let main =

    List.fold_left (fun accu conj ->

    (* Filtering out non MAIN decls *)

    (* Focusing only on MAIN_nodeid predicates *)

    if node_name = "MAIN_" ^ node_id then

      (* Extracting info *)

      (* Recall that MAIN args are 

	 main_input @ 

	 (full_memory_vars machines machine) @

	 main_output   *)

      let args = Z3.Expr.get_args conj in

      if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then

	let id = Z3.Arithmetic.Integer.get_int (List.hd args) in

	let input_values = Utils.List.extract args 1 (1 + nb_inputs) in

	let output_values = Utils.List.extract args (1+nb_inputs+nb_mems) (1 + nb_inputs + nb_mems + nb_outputs) in

	(id, (input_values, output_values))::accu

      else

	assert false

    else

      accu 

  ) [] conjuncts

  in

  let main = List.sort (fun (id1, _) (id2, _) -> compare id1 id2) main in

  List.iter (

    fun (id, expr) ->

      Format.eprintf "Id %i: %a@."

	(id)

	(Utils.fprintf_list ~sep:", "

	   (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e)))

	(fst expr)

  ) main;		    

   (* let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *)

   (* We recover the Zustre XML format, projecting each cex on each input/output

      signal *)

  let in_signals, out_signals =

    List.fold_right (

      fun (id, (sigs_in, sigs_out)) (res_sigs_in, res_sigs_out) ->

	let add l1 l2 = List.map2 (fun e1 e2 -> fst e2, ((id, e1)::(snd e2))) l1 l2 in

	let sigs_in_id = add sigs_in res_sigs_in in

	let sigs_out_id = add sigs_out res_sigs_out in

	sigs_in_id, sigs_out_id

    ) main (List.map (fun v -> v, []) inputs, List.map (fun v -> v, []) outputs)

  in

  (* let _ = List.mapi (fun k conj -> *)

  (*   (\* k-iterate *\) *)

  (*   let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *)

  (*   let func_decl = Z3.Expr.get_func_decl conj in *)

  (*   if !debug then Format.eprintf "FuncDecl %s@." (Z3.FuncDecl.to_string func_decl); *)

  (*   let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in *)

  (*   if !debug then Format.eprintf "Node %s, args %a@." node_name  (Utils.fprintf_list ~sep:", " (Format.pp_print_string)) ground_val; *)

  (*   () *)

  (*   (\*  ground_pair = [] *)

  (*           try: *)

  (*               ground_vars = pred_dict[node_name] *)

  (*               ground_pair = zip(ground_vars,ground_val) *)

  (*               if "_reset" in node_name: *)

  (*                   # this condition is to remove the node nodename_reset added by lustrec *)

  (*                   continue *)

  (*                   # node = node_name.split("_reset")[0] *)

  (*                   # cex_dict.update({node:{k:ground_pair}}) *)

  (*               elif "_step" in node_name: *)

  (*                   node = node_name.split("_step")[0] *)

  (*                   try: *)

  (*                       # case in which we already have the node in dict *)

  (*                       d = cex_dict[node] *)

  (*                       max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *)

  (*                       d.update({(max_key+1):ground_pair}) *)

  (*                   except Exception as e: *)

  (*                       self._log.warning("Adding a new node cex " + str(e)) *)

  (*                       cex_dict.update({node:{k:ground_pair}}) *)

  (*               else: *)

  (*                   node = node_name *)

  (*                   try: *)

  (*                       d = cex_dict[node] *)

  (*                       max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *)

  (*                       d.update({(max_key+1):ground_pair}) *)

  (*                   except Exception as e: *)

  (*                       if node not in ["MAIN", "ERR"]: *)

  (*                           self._log.warning("Adding a new node cex " + str(e)) *)

  (*                           cex_dict.update({node:{k:ground_pair}}) *)

  (*           except Exception as e: *)

  (*               self._log.warning("Problem with getting a node name: " + str(e)) *)

  (*   *\) *)

  (* ) conjuncts in *)

  (*   let rules_expr = Z3.Fixedpoint.get_rules !fp in *)

  (*   if !debug then *)

  (*     Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)

  (* 	(Utils.fprintf_list ~sep:"@ " *)

  (*   	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)

  (* 	rules_expr; *)

  (*   if !debug then *)

  (*     Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp); *)

  let stats_entries =   Z3.Statistics.get_entries stats in

  List.iter (fun e -> Format.eprintf "%s@.@?"

    (Z3.Statistics.Entry.to_string e)

  ) stats_entries;

  let json : Yojson.json =

    `Assoc [

      "Results",

      `Assoc [

	"Property",

	`Assoc [

	  "name", `String node_id;

	  "date", `String (Utils.get_date ());

	  "query", `Assoc ["unit", `String "sec";

			   "value", `Float (

			     let time_opt = Z3.Statistics.get stats "time.spacer.solve" in

			     match time_opt with None -> -1.

			     | Some f -> Z3.Statistics.Entry.get_float f)

			  ];

	  "answer", `String "CEX";

	  "counterexample",

	  `Assoc [

	    node_id, `Assoc

	      (

		List.map (fun (vardecl, values) ->

		  vardecl.var_id,

		  `Assoc [

		    "type", (let _ = Format.fprintf Format.str_formatter "%a" Printers.pp_var_type vardecl in

			    let s = Format.flush_str_formatter () in

			    `String s);

		    "values", `Assoc (List.map (fun (id, v) ->

		      string_of_int id, `String (Z3.Expr.to_string v))

					values)

		  ]   

		) in_signals

	      )

	  ]

	]

      ]

     ]

  in

  Format.eprintf "JSON: %s@."

    (Yojson.to_string json);

  (* Results *)

  (*   Property *)

  (*   Date *)

  (*   Query time *)

  (*   Answer CEX *)

  (*   Counterexample *)

  (*     Node name="nodeid" *)

  (*       Stream name="opt.x" type="unk" *)

  (* 	  Value instant="0">xxx</Value>		       *)

  (* () *)

(* Local Variables: *)

(* compile-command:"make -C ../.. lustrev" *)

(* End: *)

      if not !param_pp then (

	(* Mandatory to print all steps and recover cex *)

      (* P.add_bool fp_params (mks "print_certificate") true; *)

      P.add_bool fp_params (mks "xform.slice") false ; (* required to preserve signatures *)

      (* P.add_bool fp_params (mks "print_statistics") true; *)

      (* P.add_bool fp_params (mks "print_certificate") true;  *)

	let queries = Z3.Fixedpoint.parse_file !fp "nstep.smt2" in

	let decl_err = List.hd queries in

      	let res_status = Z3.Fixedpoint.query !fp decl_err in

	Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);

	(* let _ =  *)

	(*   match res_status with *)

	(*   | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err *)

	(*   | _ -> () *)

	(* in *)

	exit 0

(* compile-command:"make -C ../.. lustrev" *)

  let rec extract l fst last =

    if last < fst then assert false else

      match l, fst with

      | hd::tl, 0 -> if last = 0 then [] else hd::(extract tl 0 (last-1))

      | _::tl, _ -> extract tl (fst-1) (last-1)

      | [], 0 -> if last=0 then [] else assert false (* List too short *)

      | _ -> assert false 

let get_date () =

  let tm = Unix.localtime (Unix.time ()) in

  let fmt = Format.str_formatter in

  let open Unix in

  let _ =

    Format.fprintf fmt

      "%i/%i/%i %ih%i:%i"

      tm.tm_year

      tm.tm_mon

      tm.tm_mday

      tm.tm_hour

      tm.tm_min

      tm.tm_sec

  in

  Format.flush_str_formatter ()