From d0f26f049927668a1e0edb404909e710eddf1e2e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Thu, 17 Jun 2021 19:00:19 +0200
Subject: [PATCH] corrections for stateless nodes
---
dune-project | 1 +
src/backends/C/c_backend.ml | 18 +++-----
src/backends/C/c_backend_common.ml | 2 +-
src/backends/C/c_backend_header.ml | 3 +-
src/backends/C/c_backend_spec.ml | 10 +----
src/backends/C/c_backend_src.ml | 7 ++--
src/backends/Horn/horn_backend_traces.ml | 6 +--
src/clock_calculus.ml | 9 ++--
src/lustre_live.ml | 2 -
src/machine_code.ml | 53 ++++++++++++------------
src/machine_code_common.mli | 2 +
src/main_lustre_testgen.ml | 2 +-
src/typing.ml | 2 +-
13 files changed, 52 insertions(+), 65 deletions(-)
diff --git a/dune-project b/dune-project
index 6b6ecc3c..b24676ef 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,5 @@
(lang dune 2.8)
+
(name lustrec)
(version 1.7)
diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index 04f1f6de..f3008056 100644
--- a/src/backends/C/c_backend.ml
+++ b/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;
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 621edbd4..4abd0122 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/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
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 999ea58c..6343c0aa 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/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
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 70dec97e..505a58b8 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/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
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index e7711d4d..8e9fa4f0 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/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) ->
diff --git a/src/backends/Horn/horn_backend_traces.ml b/src/backends/Horn/horn_backend_traces.ml
index 5cc92914..6c26620b 100644
--- a/src/backends/Horn/horn_backend_traces.ml
+++ b/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 =
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index dd72307c..9cb97068 100644
--- a/src/clock_calculus.ml
+++ b/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 _ ->
diff --git a/src/lustre_live.ml b/src/lustre_live.ml
index f38e65cd..6e66609a 100644
--- a/src/lustre_live.ml
+++ b/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 =
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 9251adcc..44645a32 100644
--- a/src/machine_code.ml
+++ b/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
{
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index 081fe193..254ccd55 100644
--- a/src/machine_code_common.mli
+++ b/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
diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml
index 36b6fdb8..27f2de55 100644
--- a/src/main_lustre_testgen.ml
+++ b/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 _
diff --git a/src/typing.ml b/src/typing.ml
index b69b2b8f..4f5cda9c 100644
--- a/src/typing.ml
+++ b/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)))
--
GitLab