CristalCaveGem » LustreC

  | Types.Tstatic _

  | Types.Tconst _

  | Types.Tarrow _

                             Types.print_ty t; assert false

  Format.fprintf fmt "(declare-var %s %a)"

    id.var_id

    pp_type id.var_type

let pp_var fmt id = Format.pp_print_string fmt id.var_id

    [] -> assert false

  | [x] -> pp fmt x

  | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l

let rename f = (fun v -> {v with var_id = f v.var_id } )

let rename_machine p = rename (fun n -> concat p n)

let rename_machine_list p = List.map (rename_machine p)

let rename_current =  rename (fun n -> n ^ "_c")

let rename_current_list = List.map rename_current

let rename_next = rename (fun n -> n ^ "_x")

let rename_next_list = List.map rename_next

let full_memory_vars machines machine =

  let rec aux fst prefix m =

    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @

	if name = "_arrow" then accu else

	  let machine_n = get_machine machines name in

	( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu

  in

  aux true machine.mname.node_id machine

  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@

    (rename_machine_list m.mname.node_id m.mstep.step_outputs)

  (stateless_vars machines m)@

(********************************************************************************************)

(*                    Instruction Printing functions                                        *)

(********************************************************************************************)

let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =

  match v with

    | Cst c         -> pp_horn_const fmt c

    | Access _ -> assert false (* no arrays *)

    | Power (v, n)  -> assert false

    | LocalVar v    -> pp_var fmt (rename_machine self v)

    | StateVar v    ->

      if Types.is_array_type v.var_type

      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))

    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl

*)

let pp_assign m self pp_var fmt var_type var_name value =

  fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value

    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =

    begin

      let (n,_) = List.assoc i m.minstances in

      match node_name n, inputs, outputs with

          pp_assign

   	    m

   	    self

	    fmt

   	    o.var_type (LocalVar o) i1

        else

          pp_assign

   	    m self (pp_horn_var m) fmt

   	    o.var_type (LocalVar o) i2

      end

	begin

	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in

	  if init then

	    Format.fprintf fmt "(%a %a%t%a%t%a)"

	      (* inputs *)

	      inputs

	      (* outputs *)

	      (List.map (fun v -> LocalVar v) outputs)

	      (Utils.pp_final_char_if_non_empty " " outputs)

	      (* memories (next) *)

	      (Utils.fprintf_list ~sep:" " pp_var) (

		  (rename_next_list (full_memory_vars machines target_machine)

	       )

	  else

	    Format.fprintf fmt "(%a %a%t%a%t%a)"

	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs

	      (List.map (fun v -> LocalVar v) outputs)

	      (Utils.pp_final_char_if_non_empty " " outputs)

	      (Utils.fprintf_list ~sep:" " pp_var) (

		   (rename_current_list (full_memory_vars machines target_machine))

		     (rename_next_list (full_memory_vars machines target_machine))

	       )

	end

    end

    with Not_found -> ( (* stateless node instance *)

      let (n,_) = List.assoc i m.mcalls in

      Format.fprintf fmt "(%s %a%t%a)"

	(node_name n)

	inputs

	(List.map (fun v -> LocalVar v) outputs)

    )

    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el

and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =

  | MReset i ->

    pp_machine_init m self fmt i

  | MLocalAssign (i,v) ->

    pp_assign

      m self (pp_horn_var m) fmt

      i.var_type (StateVar i) v

    assert false (* This should not happen anymore *)

  | MStep (il, i, vl) ->

    pp_instance_call machines ~init:init m self fmt i vl il

(**************************************************************)

   two functions: m_init and m_step

   - m_init is a predicate over m memories

   - m_step is a predicate over old_memories, inputs, new_memories, outputs

   We first declare all variables then the two /rules/.

*)

  let pp_instr init = pp_machine_instr machines ~init:init m in

    (* We don't print arrow function *)

    ()

      Format.fprintf fmt "; %s@." m.mname.node_id;

   (* Printing variables *)

     ((step_vars machines m)@

	 (rename_machine_list m.mname.node_id m.mstep.step_locals));

   Format.pp_print_newline fmt ();

   if is_stateless m then

     begin

       (* Declaring single predicate *)

       Format.fprintf fmt "(declare-rel %a (%a))@."

	 pp_machine_stateless_name m.mname.node_id

	 (List.map (fun v -> v.var_type) (stateless_vars machines m));

       (* Rule for single predicate *)

       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."

			     The node is stateless. *)

		     m.mname.node_id)

	 )

	 pp_machine_stateless_name m.mname.node_id

	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);

     end

     begin

       (* Declaring predicate *)

       Format.fprintf fmt "(declare-rel %a (%a))@."

	 pp_machine_init_name m.mname.node_id

	 (List.map (fun v -> v.var_type) (init_vars machines m));

       Format.fprintf fmt "(declare-rel %a (%a))@."

	 pp_machine_step_name m.mname.node_id

	 (List.map (fun v -> v.var_type) (step_vars machines m));

       Format.pp_print_newline fmt ();

       (* Rule for init *)

       | [] -> ()

       | assertsl -> begin

	 let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in

	 Format.fprintf fmt "; Asserts@.";

	 Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@."

	   (pp_conj pp_val) assertsl;

	 Format.fprintf fmt "; Asserts for init@.";

	 Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@."

	   (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs

	   pp_machine_init_name m.mname.node_id

	   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m)

	 Format.fprintf fmt "; Asserts for step@.";

	 Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@."

	   (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs

      	 *)

       end

       );

(*

       match m.mspec with

	 None -> () (* No node spec; we do nothing *)

       (* For the moment, we only deal with simple case: single ensures, no other parameters *)

	   ()

	 )

       | _ -> () (* Other cases give nothing *)

     end

    end

    let main_output =

     rename_machine_list machine.mname.node_id machine.mstep.step_outputs

    in

     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs

    in

      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @

      main_output

    in

      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @

      main_output_dummy

    in

    (* Special case when the main node is stateless *)

      if is_stateless machine then

	pp_machine_stateless_name, pp_machine_stateless_name

      else

    in

    Format.fprintf fmt "(declare-rel MAIN (%a))@."

      (List.map (fun v -> v.var_type) main_memory_next);

    Format.fprintf fmt "; Initial set@.";

    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";

    Format.fprintf fmt "(rule INIT_STATE)@.";

    Format.fprintf fmt "; Inductive def@.";

    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;

      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."

      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current

      step_name node

      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)

let check_prop machines fmt node machine =

  let main_output =

    rename_machine_list machine.mname.node_id machine.mstep.step_outputs

  in

    (rename_next_list (full_memory_vars machines machine)) @ main_output

  in

  Format.fprintf fmt "; Property def@.";

    (pp_conj pp_var) main_output

    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next

    ;

let cex_computation machines fmt node machine =

    let cex_input =

     rename_machine_list machine.mname.node_id machine.mstep.step_inputs

    in

     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs

    in

    let cex_output =

     rename_machine_list machine.mname.node_id machine.mstep.step_outputs

    in

     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs

    in

      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output

    in

      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy

    in

    (* Special case when the cex node is stateless *)

      if is_stateless machine then

	pp_machine_stateless_name, pp_machine_stateless_name

      else

    in

    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."

      (List.map (fun v -> v.var_type) cex_memory_next);

    Format.fprintf fmt "; Initial set@.";

    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."

      init_name node

    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)

    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;

    Format.fprintf fmt "(declare-var cexcpt Int)@.";

      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."

      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current

      step_name node

      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)

let get_cex machines fmt node machine =

    let cex_input =

    let cex_output =

     rename_machine_list machine.mname.node_id machine.mstep.step_outputs

    in

    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output

  in

  Format.fprintf fmt "; Property def@.";

    (pp_conj pp_var) cex_output

    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next

    ;

  begin

    let node = !Options.main_node in

    let machine = get_machine machines node in

    collecting_semantics machines fmt node machine;

    check_prop machines fmt node machine;

end

let translate fmt basename prog machines =

  List.iter (print_machine machines fmt) (List.rev machines);

let traces_file fmt basename prog machines =

    "; Horn code traceability generated by %s@.; SVN version number %s@.@."

    Version.number;

  (* We extract the annotation dealing with traceability *)

      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in

      in

      let content = List.map snd filtered in

      (* Elements are supposed to be a pair (tuple): variable, expression *)

	| [], Expr_tuple [v;e] -> (

	  | _ -> assert false )

	| _ -> assert false)

	content

    in

    m, traces

  ) machines

  let compute_mems m =

    let rec aux fst prefix m =

      (List.map (fun mem -> (prefix, mem)) m.mmemory) @

	  if name = "_arrow" then accu else

	    let machine_n = get_machine machines name in

	    @ accu

    in

    aux true [] m

  in

  List.iter (fun m ->

    Format.fprintf fmt "; Node %s@." m.mname.node_id;

	let machine = match p with | [] -> m | (_,m')::_ -> m' in

	let traces = List.assoc machine machines_traces in

	if List.mem_assoc v.var_id traces then

	else

	  (* We keep the variable as is: we create an expression v *)

	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)

    in

    let memories_next = (* We remove the topest pre in each expression *)

	    assert false)

	memories_old

    in

      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)

      (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")

      (Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);

  ) (List.rev machines);

(* Local Variables: *)

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

let witnesses = ref false

let optimization = ref 2

let horntraces = ref false

let options =

  [ "-d", Arg.Set_string dest_dir,

    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";

    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";

    "-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend.";

    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";

    "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";

    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";

	    )

    with Sys_error _ -> Unix.mkdir dir 0o750

  in

(* Local Variables: *)

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