CristalCaveGem » LustreC

(* EMF backend *)

(* This backup is initially motivated by the need to express Spacer computed

   invariants as Matlab Simulink executable evidences.

   Therefore the input language is more restricted. We do not expect fancy

   datastructure, complex function calls, etc.

   In case of error, use -node foo -inline to eliminate function calls that are

   not seriously handled yet.

   In terms of algorithm, the process was initially based on printing normalized

   commits (eg in dd71e482a9d0).

   A (normalized) node becomes a JSON struct

   node foo (in1, in2: int) returns (out1, out2: int);

   var x : int;

   let

   x = bar(in1, in2); -- a stateful node

   out1 = x;

   out2 = in2;

   tel

   extended with a reset input. When the node is reset, each of its "pre" expression

   is reset as well as all calls to stateful node it contains. 

   "foo": {"kind":  "stateful",

   inputs:  [{name: "in1", type: "int"}, 

   {name: "in2", type: "int"}, 

   ],

   outputs: [{name: "out1", type: "int"}, {name: "out2", type: "int"}],

   locals:  [{name: "x", type: "int"}],

   instrs:  {

   def_x: { lhs: ["x"], 

   rhs: {type: "statefulcall", name: "bar", 

   args: [in1, in2], reset: [ni4_reset] } 

   }

   def_out1: { lhs: "out1", rhs: "x" } ,

   def_out2: { lhs: "out2", rhs: "in2"}

   }

   }

   1. local assign of a variable to another one:

   def_out1: { kind: "local_assign", lhs: "out1", rhs: "x" },

   def_pre_x: { kind: "pre", lhs: "pre_x", rhs: "x" },

   3. arrow constructs, while there is not specific input, it could be reset 

   by a specific signal. We register it as a fresh rhs var:

   def_arrow: { kind: "arrow", name: "ni4", lhs: "is_init", rhs: "reset_ni4"}

   2. call to a stateless function, typically an operator

   def_x: { kind: "statelesscall", lhs: ["x"], 

   name: "bar", rhs: [in1, in2]} 

   or in the operator version 

   def_x: { kind: "operator", lhs: ["x"], 

   name: "+", rhs: [in1, in2]} 

   In Simulink this should introduce a subsystem in the first case or a 

   regular block in the second with card(lhs) outputs and card{args} inputs.

   3. call to a stateful node. It is similar to the stateless above, 

   with the addition of the reset argument

   { def_x: { kind: "statefulcall", lhs: ["x"], 

   name: "bar", rhs: [in1, in2], reset: [ni4_reset] } 

   }

   In lustrec compilation phases, a unique id is associated to this specific

   instance of stateful node "bar", here ni4. 

   Instruction such as reset(ni4) or noreset(ni4) may -- or not -- reset this 

   specific node. This corresponds to "every c" suffix of a node call in lustre.

   In Simulink this should introduce a subsystem that has this extra reset input.  

   The reset should be defined as an "OR" over (1) the input reset of the parent 

   node, __reset in the present example and (2) any occurence of reset(ni4) in 

   the instructions.

   4. branching construct: (guard expr, (tag, instr list) list)

   "merge_XX": { type: "branch", guard: "var_guard", 

   inputs:   ["varx", "vary"],

   outputs:  ["vark", "varz"],

   branches: {"tag1": {liste_of_definitions (1-4)}, ...}

   }

   In Simulink, this should become one IF block to produce enable ports 

   "var_guard == tag1", "var_guard == tag2", .... as well as one action 

   block per branch: each of these action block shall  

open Machine_code_types

open EMF_common

exception Unhandled of string

module ISet = Utils.ISet

let fprintf_list = Utils.fprintf_list

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

   -> false *)

let is_arrow_fun m i =

  match Corelang.get_instr_desc i with

       try

	 | "_arrow", [v1; v2] -> (

	   match v1.value_desc, v2.value_desc with

	   | Cst c1, Cst c2 ->

	      if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then

		true

	      else

		assert false (* only handle true -> false *)

	   | _ -> assert false

	 )

	 | _ -> false

       with

       | Not_found -> false (* Not declared (should have been detected now, or

			       imported node) *)

     )

let is_resetable_fun lustre_eq =

  (* We extract the clock if it exist from the original lustre equation *)

  match lustre_eq with

  | Some eq -> (

    match eq.eq_rhs.expr_desc with

    | Expr_appl(_,_,reset) -> (

      match reset with None -> false | Some _ -> true

    )

    | _ -> Format.eprintf "reseting expr %a@.@?" Printers.pp_expr eq.eq_rhs; assert false

  | None -> assert false (* should have been assigned to an original lustre equation *)

(*   Printing machine code as EMF             *)

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

let get_instr_id fmt i =

  match Corelang.get_instr_desc i with

  (* TODO: handle clear_reset *)

  | MClearReset -> ()

     print_protect fmt 

       (fun fmt -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)

      ISet.union accu_def common_def_vars,

      VSet.union accu_read read_vars)

    (ISet.empty, ISet.empty, VSet.empty) il

     only called on MBranch instructions but evaluate recursively

     instructions appearing in branches.

     It is used to gather the global input/output of a switch and

     print it at the begin of the JSON subtree.

     The set "All outputs" is used to filter out input variables

     belong to that set. *)

     let is_stateful = List.mem_assoc f m.minstances in 

       List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args in

       if is_stateful && is_resetable_fun i.lustre_eq then

	 let reset_var =

	   let loc = Location.dummy_loc in

	   Corelang.mkvar_decl loc

	     (reset_name f,

	      Corelang.mktyp loc Tydec_bool, Corelang.mkclock loc Ckdec_any,

	      false,

	 in

	 VSet.add reset_var args_vars

       else

	 args_vars

     )

     let read_guard = get_expr_vars g in

	   let all_writes_il, writes_il, reads_il = branch_block_vars m il in

     in

        of the branch. It may happen that a variable is defined in one

        but not in the other, because of reset for example.  

        def_vars are variables defined in all branches. *)

  | MNoReset ni ->

    let write = ISet.singleton (reset_name ni) in

    write, write, VSet.empty

  | MClearReset | MResetAssign _ -> ISet.empty, ISet.empty, VSet.empty

   guards so they can be easier merged *)

let merge_branches instrs =

  let instrs, branches =

    List.fold_right (fun i (il, branches) ->

      match Corelang.get_instr_desc i with

	MBranch _ -> il, i::branches

      | _ -> i::il, branches

    ) instrs ([],[])

  in

  let sorting_branches b1 b2 =

    match Corelang.get_instr_desc b1, Corelang.get_instr_desc b2 with

    | _ -> assert false

  in

  let sorted_branches = List.sort sorting_branches branches in

    match Corelang.get_instr_desc i with

      begin match expr.value_desc with

        | Fun (fun_id, vl) ->

          (* Thanks to normalization, vl shall only contain constant or

             local/state vars but not calls to other functions *)

          fprintf fmt "\"kind\": \"operator\",@ ";

          fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;

          fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"

            fun_id

            (pp_emf_cst_or_var_list m) vl

        | Array _ | Access _ | Power _

        | Cst _

        | Var _ ->

          fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"

            pp_var_name lhs

            (pp_emf_cst_or_var m) expr

        | ResetFlag ->

          (* TODO: handle reset flag *)

          assert false

      end

    | MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a

            pp_var_name lhs

            (pp_emf_cst_or_var m) expr

        )

            (reset_name id)

        )

      -> (

            (reset_name id)

        )

    (* TODO: handle clear_reset and reset flag *)

    | MClearReset | MResetAssign _ -> ()

        let all_outputs, outputs, inputs = branch_instr_vars m i in

        (* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *)

        (* 	Machine_code.pp_instr i *)

        (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) *)

        (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs) *)

        (* 	pp_emf_vars_decl *)

        (* 	(VSet.elements inputs) *)

        (* ; *)

        let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in

      (* 	pp_emf_vars_decl *)

      (* 	(VSet.elements inputs) *)

      fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl

	(* (let guard_inputs = get_expr_vars g in

	   VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to

	   remove guard's variable from inputs *)

	(VSet.elements inputs)

      ;

      fprintf fmt "@[<v 2>\"branches\": {@ @[<v 0>%a@]@]@ }"

	(fprintf_list ~sep:",@ "

	   (fun fmt (tag, instrs_tag) ->

	     fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl (VSet.elements branch_inputs); 

	     fprintf fmt "@[<v 2>\"instrs\": {@ ";

	     (pp_emf_instrs m) fmt instrs_tag;

	     fprintf fmt "@]@ }";

	     fprintf fmt "@]@ }"

	   )

	)

	hl

    )

      fprintf fmt "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \"%s\""

	f

	pp_var_name var

	(reset_name f)

    )

    | MStep (outputs, f, inputs) when not (is_imported_node f m) -> (

      fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%a\",@ \"id\": \"%s\",@ "

	(if is_stateful then "statefulcall" else "statelesscall")

	print_protect (fun fmt -> pp_print_string fmt (node_f.node_id)) 

	f;

      fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"

	(fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" pp_var_name v)) outputs

	fprintf fmt ",@ \"reset\": { \"name\": \"%s\", \"resetable\": \"%b\"}"

	  (reset_name f)

    )

    | MStep(outputs, f, inputs ) -> (* This is an imported node *)

       EMF_library_calls.pp_call fmt m f outputs inputs

  in

    fprintf fmt "@]@]@ }"

let pp_emf_annot cpt fmt (key, ee) =

  let _ =

    fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }"

      !cpt

      (fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s)) key

      pp_emf_eexpr ee

  in

  incr cpt

let pp_emf_spec_mode fmt m =

  fprintf fmt "{@[";

  fprintf fmt "\"mode_id\": \"%s\",@ "

    m.mode_id;

  fprintf fmt "@]}"

let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode

let pp_emf_spec_import fmt i =

  fprintf fmt "{@[";

  fprintf fmt "\"contract\": \"%s\",@ "

    i.import_nodeid;

  fprintf fmt "\"inputs\": [%a],@ "

let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import

let pp_emf_spec fmt spec =

  fprintf fmt "{ @[<hov 0>";

   *   pp_emf_consts spec.consts;

   * fprintf fmt "\"locals\": [%a],@ "

   *   pp_emf_vars_decl spec.locals;

   * fprintf fmt "\"stmts\": [%a],@ "

   *   pp_emf_stmts spec.stmts; *)

    pp_emf_eexprs spec.assume;

  fprintf fmt "\"guarantees\": [%a],@ "

    pp_emf_eexprs spec.guarantees;

   *   pp_emf_spec_imports spec.imports;   *)

let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots

let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list

 *   let c = Printers.node_as_contract nd in

 *   fprintf fmt "@[<v 2>\"%a\": {@ "

 *     print_protect (fun fmt -> pp_print_string fmt nd.node_id);

 *   fprintf fmt "\"contract\": %a@ "

 *     pp_emf_spec c;

 *   fprintf fmt "@]@ }" *)

     | Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ "

     | _ -> ());

	then fprintf fmt "\"stateful\""

    fprintf fmt "\"inputs\": [%a],@ "

      pp_emf_vars_decl m.mstep.step_inputs;

    fprintf fmt "\"outputs\": [%a],@ "

      pp_emf_vars_decl m.mstep.step_outputs;

    fprintf fmt "\"locals\": [%a],@ "

      pp_emf_vars_decl m.mstep.step_locals;

    fprintf fmt "\"mems\": [%a],@ "

      pp_emf_vars_decl m.mmemory;

     | None -> ()

     | Some (Contract c) -> (

         assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []);

         fprintf fmt "\"spec\": %a,@ " pp_emf_spec c

       )

     | Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id

  with Unhandled msg -> (

    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "

      m.mname.node_id;

    eprintf "%s@ " msg;

    eprintf "node skipped - no output generated@ @]@."

  )

  | None | Some (NodeSpec _) -> pp_machine fmt m

 *)

  let ind = Corelang.imported_node_of_top top in

      print_protect (fun fmt -> pp_print_string fmt ind.nodei_id);

    fprintf fmt "\"imported\": \"true\",@ ";

    fprintf fmt "\"inputs\": [%a],@ "

      pp_emf_vars_decl ind.nodei_inputs;

    fprintf fmt "\"outputs\": [%a],@ "

      pp_emf_vars_decl ind.nodei_outputs;

    (match ind.nodei_spec with None -> fprintf fmt "@ "

  with Unhandled msg -> (

    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "

      ind.nodei_id;

    eprintf "%s@ " msg;

    eprintf "node skipped - no output generated@ @]@."

  )

(* Main function: iterates over node and print them *)

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

let pp_meta fmt basename =

  fprintf fmt "\"meta\": @[<v 0>{@ ";

  Utils.fprintf_list ~sep:",@ "

    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)

    fmt

    ["compiler-name", (Filename.basename Sys.executable_name);

     "compiler-version", Version.number;

     "command", (String.concat " " (Array.to_list Sys.argv));

     "source_file", basename

    ]

  ;

  fprintf fmt "@ @]},@ "

  fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ "

    (pp_emf_list pp_emf_typedef) (Corelang.get_typedefs prog);

  fprintf fmt "\"consts\": [@[<v 0>%a@]],@ "

    (pp_emf_list pp_emf_top_const) (Corelang.get_consts prog);

  fprintf fmt "\"imported_nodes\": @[<v 0>{@ ";

  pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog);

  fprintf fmt "}@],@ ";

     fprintf_list ~sep:",@ " pp_decl fmt prog; *)

(* Local Variables: *)

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

(* End: *)