From 9dc629947b234874c20667032b8f8e2d41cb4ea3 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 14 Feb 2024 18:18:20 -0600 Subject: [PATCH] Make circularity check more conservative For imported nodes and functions we make the conservative assumption that each output stream is dependent on the current values of all the inputs. The user must refine the model to rule out false positives. --- doc/usr/source/2_input/1_lustre.rst | 6 ++++++ src/lustre/lustreAstDependencies.ml | 12 ++++++------ .../cyclic_imported_node_call.lus} | 0 3 files changed, 12 insertions(+), 6 deletions(-) rename tests/regression/{success/possibly_cyclic_imported_node_call.lus => error/cyclic_imported_node_call.lus} (100%) diff --git a/doc/usr/source/2_input/1_lustre.rst b/doc/usr/source/2_input/1_lustre.rst index 6078c38c0..3ecb4f4db 100644 --- a/doc/usr/source/2_input/1_lustre.rst +++ b/doc/usr/source/2_input/1_lustre.rst @@ -798,6 +798,12 @@ is used. In a modular analysis, ``imported`` nodes will not be analyzed, although if their contract has modes they will be checked for exhaustiveness, consistently with the usual Kind 2 contract workflow. +Every output of an imported node is assumed to depend on every input. +This may lead Kind 2 to detect circular dependencies that do not exist +in an _actual_ system, resulting in the rejection of an input model. +To make Kind 2 accept such model, the imported node must be refined +by decomposing it into smaller subnodes and specifying the actual +dependencies among inputs and outputs. Partially defined nodes VS ``imported`` diff --git a/src/lustre/lustreAstDependencies.ml b/src/lustre/lustreAstDependencies.ml index 4d7920d1f..aead1599c 100644 --- a/src/lustre/lustreAstDependencies.ml +++ b/src/lustre/lustreAstDependencies.ml @@ -108,9 +108,9 @@ type node_summary = ((int list) IntMap.t) IMap.t we would substitute the indices with the actual call parameters during the circularity analysis for equations. - For functions and imported nodes we assume that - output streams do not depend on any of the input streams. - This restriction is in place to avoid rejecting valid programs. + For imported nodes and functions we make the conservative assumption + that each output stream is dependent on the current values + of all the arguments. We generate the node summary entry by doing a rechablility analysis for each of the output streams equations. @@ -1158,8 +1158,8 @@ let mk_node_summary: bool -> node_summary -> LA.node_decl -> node_summary s (** Computes the node call summary of the node to the input stream of the node. - For imported nodes and imported functions we assume that output streams do not depend on - any of the input streams. This restriction is in place to avoid rejecting valid programs. + For imported nodes and imported functions we assume that output streams depend on + every input stream. *) @@ -1284,7 +1284,7 @@ let check_node_equations: dependency_analysis_data = fun ad ((i, imported, params, ips, ops, locals, items, contract_opt) as ndecl)-> (if not imported then let* _ = check_no_input_output_local_duplicate ips ops locals in - analyze_circ_node_equations ad.nsummary items + analyze_circ_node_equations ad.nsummary2 items else R.ok()) >> match contract_opt with | None -> R.ok ndecl diff --git a/tests/regression/success/possibly_cyclic_imported_node_call.lus b/tests/regression/error/cyclic_imported_node_call.lus similarity index 100% rename from tests/regression/success/possibly_cyclic_imported_node_call.lus rename to tests/regression/error/cyclic_imported_node_call.lus