CristalCaveGem » LustreC

open Format

open LustreSpec

open Machine_code

open C_backend_common

open Utils

module type SPECARG = 

sig

  val prog : program 

  val machines : machine_t list

end

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

  (*                              SPEC DATATYPES                            *)

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

  type eexpr_minimachine_t = {

  muid: tag;

  mquantifiers: (quantifier_type * var_decl list) list;

  mmmemory: var_decl list;

  mmcalls: (ident * static_call) list;     (* map from stateful/stateless instance to node, 

					      no internals *)

  mminstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *)

  mminit: instr_t list;

  mmstep_logic: step_t;  

  mmstep_effects: step_t;  

  (* mmlogic: step_t;   *)

}

type spec_machine_t = {

  m_requires: eexpr_minimachine_t list;

  m_ensures: eexpr_minimachine_t list;

  m_behaviors: (string * eexpr_minimachine_t list * eexpr_minimachine_t list) list;

}

let machine_from_minimachine_effects m mm =

{

  mname = m.mname;

  mmemory = mm.mmmemory;

  mcalls = mm.mmcalls;

  minstances = mm.mminstances;

  minit = []; (* ??? *)

  mstatic = [] ; (* ??? *)

  mstep = mm.mmstep_effects;

  mspec = None;

  mannot = [];

}

let machine_from_minimachine_logics m mm =

{

  mname = m.mname;

  mmemory = mm.mmmemory;

  mcalls = mm.mmcalls;

  minstances = mm.mminstances;

  minit = []; (* ??? *)

  mstatic = [] ; (* ??? *)

  mstep = mm.mmstep_logic;

  mspec = None;

  mannot = [];

}

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

(*                       DATATYPES PRINTERS                               *)

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

let pp_acsl_type var fmt t =

  let rec aux t pp_suffix =

  match (Types.repr t).Types.tdesc with

  | Types.Tclock t'       -> aux t' pp_suffix

  | Types.Tbool           -> fprintf fmt "boolean %s%a" var pp_suffix ()

  | Types.Treal           -> fprintf fmt "real %s%a" var pp_suffix ()

  | Types.Tint            -> fprintf fmt "integer %s%a" var pp_suffix ()

  | Types.Tarray (d, t')  ->

    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in

    aux t' pp_suffix'

  (* | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix *)

  (* | Types.Tconst ty       -> fprintf fmt "%s %s" ty var *)

  (* | Types.Tarrow (_, _)   -> fprintf fmt "void (\*%s)()" var *)

  | _                     -> 

    (eprintf "internal error: pp_acsl_type %a@." Types.print_ty t; assert false)

  in aux t (fun fmt () -> ())

let pp_acsl_var_decl fmt id =

  pp_acsl_type id.var_id fmt id.var_type

let pp_quantifiers fmt (q, vars) =

  let pp_var fmt id = 

    fprintf fmt "%s: %a" id.var_id Types.print_ty id.var_type

  in

  match q with

    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 

    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 

(*

let pp_eexpr fmt ee =

  Format.fprintf fmt 

    "%a%t @[<v 2>mem      : %a@;instances: %a@;init     : %a@;logic step     :@;  @[<v 2>%a@]@;effects step     :@;  @[<v 2>%a@]@;@]@;"

    (Utils.fprintf_list ~sep:"; " pp_quantifiers) ee.mquantifiers

    (fun fmt -> match ee.mquantifiers with [] -> () | _ -> Format.fprintf fmt ";")

    (Utils.fprintf_list ~sep:", " Printers.pp_var) ee.mmmemory

    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) ee.mminstances

    (Utils.fprintf_list ~sep:"@ " pp_instr) ee.mminit

    pp_step ee.mmstep_logic

    pp_step ee.mmstep_effects

let pp_spec fmt spec =

  Format.fprintf fmt "@[<hov 2>(*@@ ";

  Utils.fprintf_list ~sep:"@;@@ " (fun fmt r -> Format.fprintf fmt "requires %a;" pp_eexpr r) fmt spec.m_requires;

  Utils.fprintf_list ~sep:"@;@@ " (fun fmt r -> Format.fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.m_ensures;

  Utils.fprintf_list ~sep:"@;" (fun fmt (name, assumes, ensures) -> 

    Format.fprintf fmt "behavior %s:@[@ %a@ %a@]" 

      name

      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> Format.fprintf fmt "assumes %a;" pp_eexpr r)) assumes

      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> Format.fprintf fmt "ensures %a;" pp_eexpr r)) ensures

  ) fmt spec.m_behaviors;

  Format.fprintf fmt "@]*)";

  ()

*)

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

(*                            CONVERTER                                   *)

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

(* The eexpr shoud have been normalized, ie. its eexpr_normalized field updated

   We add a new boolean output var and bound it to the main expression

   characterizing the eexpr.   

*)

let save_var v =

  { v with var_id = v.var_id^"_save" }

let rec postTransformLogicValue x = match x with

  | StateVar v -> StateVar (save_var v)

  | Fun (i, vl) -> Fun (i, List.map postTransformLogicValue vl)

  | Array vl -> Array (List.map postTransformLogicValue vl)

  | Access (x, y) -> Access (postTransformLogicValue x, postTransformLogicValue y)

  | Power (x, y) -> Power (postTransformLogicValue x, postTransformLogicValue y)

  | x -> x

let rec postTransformLogic x = List.map (function

    | MLocalAssign (x, y) -> MLocalAssign (x, postTransformLogicValue y)

    | MStateAssign (x, y) -> MStateAssign (x, postTransformLogicValue y)

    | MStep (x, y, z) -> MStep (x, y, List.map postTransformLogicValue z)

    | MBranch (x, y) -> MBranch (postTransformLogicValue x, List.map (function (x, y)-> (x, postTransformLogic y)) y)

    | MReset x -> MReset x

    ) x

let rec postTransformSide = function

    | MStateAssign (i, v)::q -> (MStateAssign (save_var i, StateVar i))::(MStateAssign (i, v))::(postTransformSide q)

    | t::q -> t::(postTransformSide q)

    | [] -> []

let rec postTranformMemory = function

    | t::q -> t::(save_var t)::(postTranformMemory q)

    | [] -> []

let translate_eexpr nd eexpr =

  (* Format.eprintf "Translating eexpr: %a" Printers.pp_eexpr eexpr; *)

  let output_var, eqs, locals = 

    match eexpr.eexpr_normalized with None -> assert false | Some x -> x 

  in 

  (* both inputs and outputs are considered here as inputs for the specification *) 

  let inputs = nd.node_inputs @ nd.node_outputs in

  let inputs_quantifiers = inputs @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in 

  let eexpr_local_vars = output_var :: locals @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in

  let visible_vars = eexpr_local_vars @ inputs in

  let sort_eqs inputs eqs = 

    let eqs_logic, new_locals_logic, sch_logic = Scheduling.schedule_eqs inputs visible_vars eqs in

    (* Format.eprintf "sch: [%a]@;new locals: [%a]@;locals:[%a]@.eexpr local vars: [%a]@.@?"  *)

    (*   (Utils.fprintf_list ~sep:", " Format.pp_print_string) sch_logic *)

    (*   (Utils.fprintf_list ~sep:", " Printers.pp_var) new_locals_logic *)

    (*   (Utils.fprintf_list ~sep:", " Printers.pp_var) locals *)

    (*   (Utils.fprintf_list ~sep:", " Printers.pp_var) eexpr_local_vars;  *)

    let locals = eexpr_local_vars @ new_locals_logic @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in

    let sorted_eqs_rev_logic, remainder_logic = 

      List.fold_left 

	(fun (accu, eqs_remainder) v -> 

	  if List.exists (fun eq -> List.mem v eq.eq_lhs) accu

	  then (* The variable was already handled by a previous selected eq. 

		  Typically it is part of a tuple *)

	    ((* Format.eprintf "Case 1 for variable %s@." v; *)

	     (accu, eqs_remainder)

	    )

	  else if List.exists (fun vdecl -> vdecl.var_id = v) locals || output_var.var_id = v

	  then ((* Select the eq associated to v. *) 

	    (* Format.eprintf "Case 2 for variable %s@." v; *)

	    let eq_v, remainder = find_eq v eqs_remainder in

	    eq_v::accu, remainder

	  )

	  else ((* else it is a constant value, checked during typing phase *)

	    (* Format.eprintf "Case 3 for variable %s@." v; *)

	    accu, eqs_remainder

	  )

	) 

	([], eqs_logic) 

	sch_logic 

    in

    if List.length remainder_logic > 0 then (

      Format.eprintf "Spec equations not used are@.%a@.Full equation set is:@.%a@.@?"

	Printers.pp_node_eqs remainder_logic

	Printers.pp_node_eqs eqs_logic;

      assert false );

    List.rev sorted_eqs_rev_logic, locals  

  in

  (* Generating logic definition instructions *)

  let sorted_eqs, locals = sort_eqs inputs_quantifiers eqs in

  let init_args = 

    VDSet.empty, 

    [], 

    Utils.IMap.empty, 

    List.fold_right (fun l -> VDSet.add l) locals VDSet.empty,

    [] 

  in

  let m, init, j, locals, s_logic = 

    translate_eqs 

      nd

      true (* keep_ite *)  

      eexpr_local_vars

      init_args

      (sorted_eqs) 

  in

  (* We remove side effects *)

  let s_logic = List.filter (fun i -> match i with MStateAssign _ -> false | _ -> true) s_logic in 

  (* and put the output var as the last instr *)

  let s_logic =

    let output_assign, others = 

      List.partition 

	(fun i -> match i with | MStep([v], _, _) | MLocalAssign(v,_) -> v.var_id = output_var.var_id | _ -> false)

	s_logic 

    in

    (* Format.eprintf "output instr: @.%a@.others:@.%a@." *)

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

    (*   (Utils.fprintf_list ~sep:"@." pp_instr) others; *)

    others @ output_assign

  in

  let _,_,_,_, s_side_effects = 

    translate_eqs nd true (*TODO: explose ite *)  eexpr_local_vars init_args (sorted_eqs) 

  in

  let rec filter_side_effects instrs =

    List.fold_right (

      fun i accu ->

	match i with

      | MStep([v], _, _) 

      | MLocalAssign(v,_) -> 

	if v.var_id <> output_var.var_id then

	  i::accu

	else

	  accu

      | MBranch (g, cases) -> 

	let filtered_cases = 

	  List.map (fun (l, l_instrs) -> l, filter_side_effects l_instrs) cases in

	MBranch(g, filtered_cases) :: accu

      | _ -> i::accu

    ) instrs []

  in

  let s_side_effects = filter_side_effects s_side_effects in 

  {

    muid = eexpr.eexpr_tag;

    mquantifiers = eexpr.eexpr_quantifiers;

    mmmemory = postTranformMemory (VDSet.elements m);

    mmcalls = []; (* no calls *)

    mminstances = []; (* no calls *)

    mminit = init;

    mmstep_logic = {

      step_inputs = inputs;

      step_outputs = [output_var];

      step_locals = VDSet.elements (VDSet.remove output_var (VDSet.diff locals m));

      step_checks = [] (* Not handled yet *);

      step_instrs = (

	(* special treatment depending on the active backend. For horn backend,

	   common branches are not merged while they are in C or Java

	   backends. *)

	match !Options.output with

	| "horn" -> s_logic

	| "C" | "java" | _ -> (*TODO: check that this is correct to remove : join_guards_list*) (postTransformLogic s_logic)

      );

      step_asserts = [];

    };

    mmstep_effects = {

      step_inputs = inputs; (* contains nd.node_inputs + nd.node_outputs *)

      step_outputs = nd.node_outputs; (* used by the printer to print correctly the names *)

      step_locals = VDSet.elements (VDSet.remove output_var (VDSet.diff locals m));

      step_checks = [] (* Not handled yet *);

      step_instrs = (

	(* special treatment depending on the active backend. For horn backend,

	   common branches are not merged while they are in C or Java

	   backends. *)

	match !Options.output with

	| "horn" -> s_side_effects

	| "C" | "java" | _ -> (*TODO: check that this is correct to remove : join_guards_list*) (postTransformSide s_side_effects)

      );

      step_asserts = [];

    }

  }    

let translate_spec nd spec = 

  (* Each eexpr of the spec is expressed as a minimachine: 

     instrs (to update memory and set local vars) 

     + expr (to compute the output

     + memory defs 

     + instances (for callee nodes)

  *)

  let transl = List.map (translate_eexpr nd) in

  {

    m_requires = transl spec.requires;

    m_ensures = transl spec.ensures;

    m_behaviors =

      List.map

	(fun (beh_id, req, ens, _) -> beh_id, transl req, transl ens) 

	spec.behaviors

  }

(*

mspec = Utils.option_map (translate_spec nd) nd.node_spec;

    mannot = List.flatten (

      List.map (fun ann -> List.map (fun (kwd, eexpr) -> kwd, (translate_eexpr nd eexpr)) ann.annots) nd.node_annot);

*)

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

(*                              HEADER                                    *)

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

  (* Print basic library function as ACSL functions *)

  let basic_lib_pp_acsl i get_val_type pp_val fmt vl =

    match i, vl with

    | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 

    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v

    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 

    | "impl", [v1; v2] -> Format.fprintf fmt "((!%a) ||  %a)" pp_val v1 pp_val v2 

    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2

    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 

    | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2

    | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2

    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 

    | _ -> raise (Failure ("No ACSL printer for function " ^ i))

let pp_acsl_tag fmt t =

 pp_print_string fmt (if t = Corelang.tag_true then "\\true" else if t = Corelang.tag_false then "\\false" else t)

let rec pp_acsl_const fmt c =

  match c with

    | Const_int i     -> pp_print_int fmt i

    | Const_real r    -> pp_print_string fmt r

    | Const_float r   -> pp_print_float fmt r

    | Const_tag t     -> pp_acsl_tag fmt t

    | Const_array ca  -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca

    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl

    | Const_string _ -> assert false (* string occurs in annotations not in C *)

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

    match v with

    | Cst c         -> pp_acsl_const fmt c

    | Array _      

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

    | Power (v, n)  -> assert false

    | LocalVar v    -> pp_var fmt v

    | StateVar v    ->     

      (match (Types.repr v.var_type).Types.tdesc with

      | Types.Tbool           -> fprintf fmt "((%t)?\\true:\\false)"

      | _ -> fprintf fmt "%t")

      (if Types.is_array_type v.var_type

      then assert false

      else fun fmt -> fprintf fmt "%s%s_reg.%s" self 

     (if !Options.no_pointer then "." else "->") v.var_id)

    | Fun (n, vl)   -> Format.fprintf fmt "%a" (basic_lib_pp_acsl n Machine_code.get_val_type (pp_acsl_val self pp_var)) vl

  let rec pp_eexpr_logic_instr m eem fmt instr =

    let self = mk_self m in

    let conv_m =  machine_from_minimachine_logics m eem in

    match instr with 

    | MReset i -> assert false (* should not happen, calls were inlined *)

    | MLocalAssign (i,v) -> (

      match conv_m.mstep.step_outputs with 

      | [o] -> if i = o then

	  fprintf fmt "%a;" (pp_acsl_val self (pp_c_var_read conv_m)) v

	else

	  fprintf fmt "\\let %a = %a;" 

	    (pp_c_var_read conv_m (* TODO no variable shold be treated as output *)) i

	    (pp_acsl_val self (pp_c_var_read conv_m)) v

      | _ -> 

	assert false (* should not happen: only a single output *)

    )

    | MStateAssign (i,v) -> 

      assert false (* should not happen, no side effects in logical predicates *)

    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->

      pp_eexpr_logic_instr m eem fmt (MLocalAssign (i0, Fun (i, vl)))

  | MStep ([i0], "ite", vl) ->

    pp_eexpr_logic_instr m eem fmt (MLocalAssign (i0, Fun ("ite", vl)))

  | MStep (il, i, vl) ->

    Format.eprintf "Illegal function call %s@.%a@.@?" i pp_instr instr; 

    assert false (* should not happen, calls were inlined *)

  | MBranch (g,hl) -> assert false (* should not happen. Oder ??? TODO *)

let pp_logic_eexpr m fmt ee =

  fprintf fmt "%a%t%a"

    (Utils.fprintf_list ~sep:"@ " pp_quantifiers) ee.mquantifiers

    (Utils.pp_final_char_if_non_empty " " ee.mquantifiers) 

    (Utils.fprintf_list ~sep:"@;" 

       (pp_eexpr_logic_instr m ee)) ee.mmstep_logic.step_instrs

let pp_acsl_spec_logics stateless m fmt spec = 

  let self = mk_self m in

  let pp_expr_def fmt ee =

    match ee.mmstep_logic.step_instrs with

    | [MStep([o], i, vl)] -> () (* We do nothing, the expression is simple and 

				   was introduced directly in the contract *)

    | _ -> ((* We define a new ACSL predicate *)

      fprintf fmt "/*@@ @[<v 3>predicate spec_%i(%a%t) =@;%a@]@;*/@." 

	ee.muid   

	(Utils.fprintf_list ~sep:", " pp_acsl_var_decl) ee.mmstep_logic.step_inputs

  (fun fmt -> if stateless then fprintf fmt "" else fprintf fmt "%t%a %s%s"

  (Utils.pp_final_char_if_non_empty ", " ee.mmstep_logic.step_inputs)

	pp_machine_memtype_name m.mname.node_id

  (if !Options.no_pointer then "" else "*")

	self)

	(pp_logic_eexpr m) ee

    )

  in

  List.iter (pp_expr_def fmt) 

    (spec.m_requires@

       spec.m_ensures@

       (List.fold_left 

	  (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 

	  [] spec.m_behaviors)

    )

(* Access to the value of a variable:

   - if it's not a scalar output, then its name is enough

   - otherwise, dereference it (it has been declared as a pointer,

     despite its scalar Lustre type)

   - moreover, cast arrays variables into their original array type.

*)

let pp_acsl_var_read suffix outputs fmt id =

  if Types.is_array_type id.var_type

  then

    assert false (* no array *)

  else (

    (if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)

    then fprintf fmt "((*%s)%s" id.var_id suffix

    else fprintf fmt "(%s%s" id.var_id suffix);

      match (Types.repr id.var_type).Types.tdesc with

      | Types.Tbool           -> fprintf fmt "?\\true:\\false)"

      | _ -> fprintf fmt ")"

  )

let pp_requires_mem stateless machines fmt m =

  let self = mk_self m in

  List.iter (fun v -> fprintf fmt "requires \\valid(%s);@;" v.var_id) m.mstep.step_outputs;

  let mems = Machine_code.get_mems m machines in

  (if not !Options.no_pointer then

    List.iter (fun prefix -> fprintf fmt "requires \\valid(%s%a);@;" self

      (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix

    )

      (Machine_code.get_instances m machines)

  );

  if not stateless then fprintf fmt "requires \\valid(%s);@;" self;

  if List.length mems + List.length m.mstep.step_outputs > 1 then

    fprintf fmt "requires \\separated(@[<hov>%a%t%a@]);@;" 

      (Utils.fprintf_list ~sep:",@ " 

	      (fun fmt v -> pp_print_string fmt v.var_id))

      m.mstep.step_outputs 

      (Utils.pp_final_char_if_non_empty ",@ " mems)

      (if !Options.no_pointer then

        fun fmt x -> fprintf fmt "%s" (if stateless then "" else self) (*maybe we want to add more pointers here like arrays *)

      else

        Utils.fprintf_list ~sep:",@ " (fun fmt (prefix, var) -> fprintf fmt "&%s%a->_reg.%s"

	        self 

	        (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix

	        var.var_id))

      mems

let pp_assigns more stateless machines fmt m =

  let self = mk_self m in

  let mems = Machine_code.get_mems m machines in

  fprintf fmt "assigns @[<hov>%a%a%t%a@];@;"

    (Utils.fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "*%s" v.var_id))

    m.mstep.step_outputs

    (if !Options.no_pointer then

        fun fmt mems -> fprintf fmt "%s" (if stateless then "" else (", *"^self)) (*maybe we want to keep some memory like array *)

     else Utils.fprintf_list ~sep:",@ "

       (fun fmt (prefix, var) -> fprintf fmt "%t%s%a->_reg.%s"

         (Utils.pp_final_char_if_non_empty ",@ " mems)

         self

         (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix

         var.var_id)

    )

    mems

    (Utils.pp_final_char_if_non_empty ",@ " more)

    (Utils.fprintf_list ~sep:",@ " (fun fmt v -> v fmt))

    more

let pp_acsl_mem_valid stateless pre post machines fmt m =

  fprintf fmt "@[<v 2>/*@@ ";

  pp_requires_mem stateless machines fmt m;

  pre fmt;

  post fmt;

  pp_assigns [] stateless machines fmt m;

  fprintf fmt "@]*/@.";

  ()

(* Seems to be a simplification of pp_assign (in c_backend_src *)

let pp_expr_rhs m pp_var fmt var_type value =

  let self = mk_self m in

  let depth = C_backend_src.expansion_depth value in

(*eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*)

  let loop_vars = C_backend_src.mk_loop_variables m var_type depth in

  let reordered_loop_vars = C_backend_src.reorder_loop_variables loop_vars in

  let rec aux fmt vars =

    match vars with

    | [] ->

      fprintf fmt "%a;" 

	(C_backend_src.pp_value_suffix self loop_vars pp_var) value

    | _ -> assert false

  in

  begin

    reset_loop_counter ();

    (*reset_addr_counter ();*)

    aux fmt reordered_loop_vars

  end

let pp_acsl_spec_contracts stateless pre post machines m outputs fmt spec = 

  let self = mk_self m in

    (* let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in *)

  let pp_eexpr_expr fmt ee = 

      (* If the eexpr contains a single definition we use it directly. Otherwise,

	 we rely on an external predicate *)

    let conv_m =  machine_from_minimachine_logics m ee in

    match ee.mmstep_logic.step_instrs with

    | [MStep([o], i, vl)] -> 

      fprintf fmt "%a %t"

	(Utils.fprintf_list ~sep:" " pp_quantifiers) ee.mquantifiers

	(fun fmt ->

	  let value = Fun (i, vl) in

       	  pp_expr_rhs

	    conv_m

	    (pp_c_var_read conv_m) 

	    fmt

	    o.var_type value 

	)

    | _ -> fprintf fmt "spec_%i(%a%t);" 

      ee.muid   

      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read "" outputs)) ee.mmstep_logic.step_inputs

      (fun fmt -> if stateless then fprintf fmt "" else fprintf fmt ", %s%s" (if !Options.no_pointer then "*" else "") self)

  in

  fprintf fmt "@[<v 2>/*@@ ";

  (* Valid pointers *)

  pp_requires_mem stateless machines fmt m;

  (* Spec requires *)

  Utils.fprintf_list ~sep:"" 

    (fun fmt r -> fprintf fmt "requires %a@ " pp_eexpr_expr r) 

    fmt 

    spec.m_requires;

  pre fmt;

  Utils.fprintf_list ~sep:"" 

    (fun fmt r -> fprintf fmt "ensures %a@ " pp_eexpr_expr r) 

    fmt 

    spec.m_ensures;

  post fmt;

  fprintf fmt "@ ";

    (* TODO assigns + separated *)

    (* fprintf fmt "assigns *self%t%a;@ "  *)

    (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)

    (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)

    Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, ensures) -> 

      fprintf fmt "behavior %s:@[@ %a@ %a@]" 

	name

	(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a" pp_eexpr_expr r)) assumes

	(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a" pp_eexpr_expr r)) ensures

    ) fmt spec.m_behaviors;

    (* Assings *)

    pp_assigns [] stateless machines fmt m;

    fprintf fmt "@]@ */@.";

    ()

let pp_c_decl_struct_spec_var fmt id =

  if !Options.ghost_mode then

    fprintf fmt "/*@@ ghost %a */" pp_c_decl_struct_var id

 else 

    fprintf fmt "%a" pp_c_decl_struct_var id

module Make = 

  functor (SpecArg: SPECARG) -> 

struct

  open SpecArg

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

(*                              INITIALIZE DATA                           *)

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

(* Map each machine uid to its compiled spec (and TODO later annot) *)

let compiled_contracts : (node_desc * spec_machine_t) list ref = ref []

let compiled_ee : eexpr_minimachine_t list ref = ref []

let init machines =

  List.iter (

    fun m -> (* iterate through spec eexpr and register them *)

      let nd = m.mname in

      let translate_eexpr ee = 

	        let eem = translate_eexpr nd ee in

	        compiled_ee := eem::!compiled_ee;

	        eem

      in

      let tl = List.map translate_eexpr in

      match m.mspec with

      | None -> ()

      | Some spec ->

	let compiled_spec =

	  { m_requires = tl spec.requires;

	    m_ensures =  tl spec.ensures;

	    m_behaviors = List.map 

	      (fun (s, eel1, eel2, _) -> (s, tl eel1, tl eel2))

	      spec.behaviors

	  }

	in

	compiled_contracts := (nd, compiled_spec)::!compiled_contracts

  ) machines

let get_ee_minimachine ee = 

  List.find (fun eem -> eem.muid = ee.eexpr_tag) !compiled_ee 

let get_spec nd = List.assoc nd !compiled_contracts

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

(*                              HEADER                                    *)

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

module HdrMod = struct

let get_spec_memories m =

  match m.mspec with

    None -> []

  | Some _ -> 

    let spec = get_spec m.mname in

    List.flatten (

    List.map (fun ee -> ee.mmmemory) 

      (spec.m_requires@

	 spec.m_ensures@

	 (List.fold_left 

	    (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 

	    [] spec.m_behaviors)

      ))

let _print_machine_decl_init_fun_prefix pre post fmt m =

      let self = mk_self m in

	    fprintf fmt "/*@@requires \\valid(%s);@." self;

      pre fmt;

      post fmt;

	    fprintf fmt "assigns *%s;*/@." self

let _print_machine_decl_step_fun_prefix stateless pre post fmt m =

(* Print specification contracts if any *)

      (match m.mspec with

      | None -> pp_acsl_mem_valid stateless pre post machines fmt m

      | Some _ -> 

	let spec = get_spec m.mname in

    	pp_acsl_spec_contracts stateless pre post machines m m.mstep.step_outputs fmt spec

      )

let has_spec_mem m = (get_spec_memories m) <> []

let pp_registers_struct fmt m = 

  let spec_memories = get_spec_memories m in

  (Utils.fprintf_list ~sep:"@;" pp_c_decl_struct_spec_var) fmt spec_memories

let print_machine_decl_prefix fmt m =

  (* Print specification if any *)

  let mems = Machine_code.get_mems m machines in  

  (match m.mspec with

  | None -> ()

  | Some _ ->

    let spec = get_spec m.mname in

    pp_acsl_spec_logics (List.length mems == 0) m fmt spec

  )

let print_machine_decl_step_fun_prefix fmt m = _print_machine_decl_step_fun_prefix false (fun fmt -> ()) (fun fmt -> ()) fmt m

let print_machine_decl_init_fun_prefix fmt m = _print_machine_decl_init_fun_prefix (fun fmt -> ()) (fun fmt -> ()) fmt m

let print_machine_decl_stateless_fun_prefix fmt m = _print_machine_decl_step_fun_prefix true (fun fmt -> ()) (fun fmt -> ()) fmt m

let print_global_decl = fun fmt -> ()

end

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

(*                              CODE                                      *)

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

module SrcMod =

struct

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

(*                              CODE                                      *)

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

  let pp_instr_debug m (eem: eexpr_minimachine_t) fmt instrs =

    let self = mk_self m in

    let conv_m = machine_from_minimachine_effects m eem in

    Utils.fprintf_list ~sep:"@;" 

      (C_backend_src.pp_machine_instr_internal 

	 [] (* no dependencies considered *)

	 conv_m

	 (* (m.mname.node_id,  *)

	 (*  ee.mmstep_effects.step_inputs,  *)

	 (*  ee.mmstep_effects.step_outputs,  *)

	 (*  ee.mmstep_effects.step_locals,  *)

	 (*  ee.mmmemory,  *)

	 (*  ee.mminstances,  *)

	 (*  ee.mmcalls) *)

	 self)

      fmt 

      instrs

  (* Print instructions *)

  let pp_instr pp_machine_instr m (eem: eexpr_minimachine_t) fmt instrs =

    let self = mk_self m in

    let conv_m = machine_from_minimachine_effects m eem in

    Utils.fprintf_list ~sep:"@;" 

      (pp_machine_instr 

	 [] (* no dependencies considered *)

	 conv_m

	 (* (m.mname.node_id,  *)

	 (*  ee.mmstep_effects.step_inputs,  *)

	 (*  ee.mmstep_effects.step_outputs,  *)

	 (*  ee.mmstep_effects.step_locals,  *)

	 (*  ee.mmmemory,  *)

	 (*  ee.mminstances,  *)

	 (*  ee.mmcalls) *)

	 self)

      fmt 

      instrs

  let pp_acsl_spec_side_effects pp_machine_instr m fmt spec = 

    let pp_side_effects fmt ee =  

      (* Declare local vars *)

      let locals = 

	List.filter 

	  (fun l -> not (List.mem l m.mstep.step_locals)) 

	  ee.mmstep_effects.step_locals 

      in