corrections for stateless nodes

dune-project

 (lang dune 2.8)
+
 (name lustrec)
 (version 1.7)
 

src/backends/C/c_backend.ml

@@ -41,18 +41,15 @@ let gen_files
     ( print_alloc_header,
       print_lib_c,
       print_main_c,
-      print_makefile,
-      preprocess
+      print_makefile
     (* , print_cmake *) ) basename prog machines dependencies =
   let destname = !Options.dest_dir ^ "/" ^ basename in
 
-  let machines, spec = preprocess machines in
-
   (* Generating H alloc file *)
   let alloc_header_file = destname ^ "_alloc.h" in
   (* Could be changed *)
   with_out_file alloc_header_file (fun header_fmt ->
-      print_alloc_header header_fmt basename prog machines dependencies spec);
+      print_alloc_header header_fmt basename machines dependencies);
 
   (* Generating Lib C file *)
   let source_lib_file = c_or_cpp destname in
@@ -124,21 +121,19 @@ let print_c_header basename =
       Header.print_header_from_header header_fmt basename lusic.contents)
 
 let translate_to_c generate_c_header basename prog machines dependencies =
-  let header_m, source_m, source_main_m, makefile_m, preprocess =
+  let header_m, source_m, source_main_m, makefile_m =
     match !Options.spec with
     | "no" ->
       ( C_backend_header.((module EmptyMod : MODIFIERS_HDR)),
         C_backend_src.((module EmptyMod : MODIFIERS_SRC)),
         C_backend_main.((module EmptyMod : MODIFIERS_MAINSRC)),
-        C_backend_makefile.((module EmptyMod : MODIFIERS_MKF)),
-        fun m -> m, [] )
+        C_backend_makefile.((module EmptyMod : MODIFIERS_MKF)) )
     | "acsl" ->
       let open C_backend_spec in
       ( C_backend_header.((module HdrMod : MODIFIERS_HDR)),
         C_backend_src.((module SrcMod : MODIFIERS_SRC)),
         C_backend_main.((module EmptyMod : MODIFIERS_MAINSRC)),
-        C_backend_makefile.((module MakefileMod : MODIFIERS_MKF)),
-        preprocess_acsl )
+        C_backend_makefile.((module MakefileMod : MODIFIERS_MKF)) )
     | "c" ->
       assert false (* not implemented yet *)
     | _ ->
@@ -153,8 +148,7 @@ let translate_to_c generate_c_header basename prog machines dependencies =
     ( Header.print_alloc_header,
       Source.print_lib_c,
       SourceMain.print_main_c,
-      Makefile.print_makefile,
-      preprocess )
+      Makefile.print_makefile )
     (* CMakefile.print_makefile *)
   in
   if generate_c_header then print_c_header basename;

src/backends/C/c_backend_common.ml

@@ -720,7 +720,7 @@ module type MODIFIERS_GHOST_PROTO = sig
 end
 
 module EmptyGhostProto : MODIFIERS_GHOST_PROTO = struct
-  let pp_ghost_parameters ?cut _ _ = ()
+  let pp_ghost_parameters ?cut _ _ = ignore cut
 end
 
 module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct

src/backends/C/c_backend_header.ml

@@ -302,8 +302,7 @@ functor
     (* MAIN Header Printing functions *)
     (********************************************************************************************)
 
-    let print_alloc_header header_fmt basename _prog machines dependencies spec
-        =
+    let print_alloc_header header_fmt basename machines dependencies =
       (* Include once: start *)
       let baseNAME = file_to_module_name basename in
       fprintf header_fmt

src/backends/C/c_backend_spec.ml

@@ -22,10 +22,6 @@ open Machine_code_common
 
 (**************************************************************************)
 
-(* TODO ACSL Return updates machines (eg with local annotations) and acsl
-   preamble *)
-let preprocess_acsl machines = machines, []
-
 let pp_acsl_basic_type_desc t_desc =
   if Types.is_bool_type t_desc then
     (* if !Options.cpp then "bool" else "_Bool" *)
@@ -187,11 +183,7 @@ let pp_or_l pp_v fmt =
 
 let pp_not pp fmt = fprintf fmt "!%a" pp
 
-let pp_valid pp =
-  pp_and_l
-    (* pp_print_list *)
-    (* ~pp_sep:pp_print_cut *)
-    (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
+let pp_valid pp = pp_and_l (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
 
 let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
 

src/backends/C/c_backend_src.ml

@@ -228,9 +228,10 @@ functor
         | MSetReset inst ->
           pp_machine_set_reset m self mem fmt inst
         | MClearReset ->
-          fprintf fmt "%t@,%a"
-            (pp_machine_clear_reset m self mem)
-            pp_label reset_label
+          if not (fst (get_stateless_status m)) then
+            fprintf fmt "%t@,%a"
+              (pp_machine_clear_reset m self mem)
+              pp_label reset_label
         | MResetAssign b ->
           pp_reset_assign self fmt b
         | MLocalAssign (i, v) ->

src/backends/Horn/horn_backend_traces.ml

@@ -27,7 +27,7 @@ let pp_traces =
 
 (* Compute memories associated to each machine *)
 let compute_mems machines m =
-  let rec aux fst prefix m =
+  let rec aux prefix m =
     List.map (fun mem -> prefix, mem) m.mmemory
     @ List.fold_left
         (fun accu (id, (n, _)) ->
@@ -35,10 +35,10 @@ let compute_mems machines m =
           if name = "_arrow" then accu
           else
             let machine_n = get_machine machines name in
-            aux false ((id, machine_n) :: prefix) machine_n @ accu)
+            aux ((id, machine_n) :: prefix) machine_n @ accu)
         [] m.minstances
   in
-  aux true [] m
+  aux [] m
 
 (* We extract the annotation dealing with traceability *)
 let machines_traces machines =

src/clock_calculus.ml

@@ -480,19 +480,18 @@ and clock_appl env f args clock_reset loc =
 
 and clock_call env f args clock_reset loc =
   (* Format.eprintf "Clocking call %s@." f; *)
-  let cfun = clock_ident false env f loc in
+  let cfun = clock_ident env f loc in
   let cins, couts = split_arrow cfun in
   let cins = clock_list_of_clock cins in
   List.iter2 (clock_subtyping_arg env) args cins;
   unify_imported_clock (Some clock_reset) cfun loc;
   couts
 
-and clock_ident nocarrier env id loc =
-  clock_expr ~nocarrier env (expr_of_ident id loc)
+and clock_ident env id loc = clock_expr env (expr_of_ident id loc)
 
 and clock_carrier env c loc ce =
   let expr_c = expr_of_ident c loc in
-  let ck = clock_expr ~nocarrier:false env expr_c in
+  let ck = clock_expr env expr_c in
   let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
   let ckb = new_var true in
   let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in
@@ -502,7 +501,7 @@ and clock_carrier env c loc ce =
 
 (** [clock_expr env expr] performs the clock calculus for expression [expr] in
     environment [env] *)
-and clock_expr ?(nocarrier = true) env expr =
+and clock_expr env expr =
   let resulting_ck =
     match expr.expr_desc with
     | Expr_const _ ->

src/lustre_live.ml

@@ -15,8 +15,6 @@ open Utils
 open ISet
 module Live = Map.Make (Int)
 
-let pp_live fmt l = Live.bindings
-
 let assigned s eq = union s (of_list eq.eq_lhs)
 
 let rec occur_dim_expr s d =

src/machine_code.ml

@@ -236,7 +236,8 @@ let reset_instance env i r c =
   | None ->
     None, []
 
-let translate_eq env ctx id inputs locals outputs i eq =
+let translate_eq env ctx nd inputs locals outputs i eq =
+  let id = nd.node_id in
   let translate_expr = translate_expr env in
   let translate_act = translate_act env in
   let locals_pi = Lustre_live.inter_live_i_with id (i - 1) locals in
@@ -268,11 +269,12 @@ let translate_eq env ctx id inputs locals outputs i eq =
         {
           inst with
           instr_spec =
-            [
-              mk_memory_pack ~i id;
-              mk_transition ~i id (vdecls_to_vals inputs)
-                (vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);
-            ];
+            (if fst (get_stateless_status_node nd) then []
+            else [ mk_memory_pack ~i id ])
+            @ [
+                mk_transition ~i id (vdecls_to_vals inputs)
+                  (vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);
+              ];
         }
         :: ctx.s;
       mp = pred_mp ctx spec_mp;
@@ -388,10 +390,10 @@ let constant_equations locals =
       else eqs)
     [] locals
 
-let translate_eqs env ctx id inputs locals outputs eqs =
+let translate_eqs env ctx nd inputs locals outputs eqs =
   List.fold_left
     (fun (ctx, i) eq ->
-      let ctx = translate_eq env ctx id inputs locals outputs i eq in
+      let ctx = translate_eq env ctx nd inputs locals outputs i eq in
       ctx, i + 1)
     (ctx, 1) eqs
   |> fst
@@ -434,18 +436,16 @@ let process_asserts nd =
     in
     vars, eql, assertl
 
-let translate_core env nid sorted_eqs inputs locals outputs =
+let translate_core env nd sorted_eqs inputs locals outputs =
   let constant_eqs = constant_equations locals in
 
   (* Compute constants' instructions *)
-  let ctx0 =
-    translate_eqs env ctx_init nid inputs locals outputs constant_eqs
-  in
+  let ctx0 = translate_eqs env ctx_init nd inputs locals outputs constant_eqs in
   assert (ctx0.si = []);
   assert (IMap.is_empty ctx0.j);
 
   (* Compute ctx for all eqs *)
-  let ctx = translate_eqs env ctx_init nid inputs locals outputs sorted_eqs in
+  let ctx = translate_eqs env ctx_init nd inputs locals outputs sorted_eqs in
 
   ctx, ctx0.s
 
@@ -480,6 +480,12 @@ let transition_0 nd =
   }
 
 let transition_toplevel nd i =
+  let tr =
+    mk_transition nd.node_id ~i
+      (vdecls_to_vals nd.node_inputs)
+      []
+      (vdecls_to_vals nd.node_outputs)
+  in
   {
     tname = nd;
     tindex = None;
@@ -487,13 +493,8 @@ let transition_toplevel nd i =
     tlocals = [];
     toutputs = nd.node_outputs;
     tformula =
-      ExistsMem
-        ( nd.node_id,
-          Predicate (ResetCleared nd.node_id),
-          mk_transition nd.node_id ~i
-            (vdecls_to_vals nd.node_inputs)
-            []
-            (vdecls_to_vals nd.node_outputs) );
+      (if fst (get_stateless_status_node nd) then tr
+      else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));
     tfootprint = ISet.empty;
   }
 
@@ -542,8 +543,7 @@ let translate_decl nd sch =
 
   (* Translate equations *)
   let ctx, ctx0_s =
-    translate_core env nd.node_id equations nd.node_inputs locals
-      nd.node_outputs
+    translate_core env nd equations nd.node_inputs locals nd.node_outputs
   in
 
   (* Format.eprintf "ok4@.@?"; *)
@@ -578,10 +578,11 @@ let translate_decl nd sch =
   let clear_reset =
     mkinstr
       ~instr_spec:
-        [
-          mk_memory_pack ~i:0 nd.node_id;
-          mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] [];
-        ]
+        ((if fst (get_stateless_status_node nd) then []
+         else [ mk_memory_pack ~i:0 nd.node_id ])
+        @ [
+            mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] [];
+          ])
       MClearReset
   in
   {

src/machine_code_common.mli

@@ -17,6 +17,8 @@ val get_const_assign :
   Lustre_types.var_decl ->
   Machine_code_types.value_t
 
+val get_stateless_status_node : Lustre_types.node_desc -> bool * bool
+
 val get_stateless_status : Machine_code_types.machine_t -> bool * bool
 
 val get_stateless_status_top_decl : Lustre_types.top_decl -> bool * bool

src/main_lustre_testgen.ml

@@ -192,7 +192,7 @@ let _ =
 
     Arg.parse options anonymous usage
   with
-  | Parse.Error _
+  | Parse.Error
   | Types.Error (_, _)
   | Clocks.Error (_, _)
   | Error.Error _

src/typing.ml

@@ -332,7 +332,7 @@ struct
   (* Expected type ty1, got type ty2 *)
   let try_unify ?(sub = false) ?(semi = false) ty1 ty2 loc =
     try unify ~sub ~semi ty1 ty2 with
-    | Unify (t1', t2') ->
+    | Unify _ ->
       raise (Error (loc, Type_clash (ty1, ty2)))
     | Dimension.Unify _ ->
       raise (Error (loc, Type_clash (ty1, ty2)))