Uclid5-based LF Verifier #1271

lsk567 · 2022-07-03T21:16:36Z

This is a PR for an LF verifier built on top of Uclid5, which analyzes an LF program with the C target and checks whether the program violates a user-specified property. Currently, this feature is enabled when the @property annotation is used.

A corresponding benchmark suite can be found here: https://github.com/lf-lang/lf-verifier-benchmarks.

Here is a list of remaining TODOs for this PR:

Major feature TODOs:

Implement an algorithm for abstracting away in the uclid encoding components that cannot causally influence the truth value of a property.
Support local variables and multiple updates to the same variable in C reaction bodies.
[Important] Integrate with CBMC. Hopefully, let CBMC output reaction axioms.

Minor features / bugs TODOs:

[LF] [!] Support physical actions (solver currently blocks).
[LF] When checking the intervals of a temporal operator, do not take microsteps into account.
[LF] If a reaction is triggered by startup, it cannot be triggered by another trigger yet.
[LF] Unconnected input ports currently have nondeterministic behavior. It should not have any signals.
[LF] Support reactor parameters.
[LF] Support multiple reactions sensitive to the same trigger.
[LF] Allow a reaction to be triggered by startup and other triggers. For example in PingPong.lf.
[LF] Support reactor parameters.
[LF] Support modal models.
[LF & C] [!] Unused triggers (e.g. a logical action declared at the LF layer but not referenced in the reaction body) can block the model. Need to handle this either in the translation or in the encoding. Even if one branch of an if statement is not using it, the entire model is blocked.

reaction(startup, serve) -> send {=
    lf_set(send, self->pingsLeft);
    self->pingsLeft -= 1;
=}

[C] Empty reaction bodies are not supported yet.
[C] [50%] Support adding an additional delay when scheduling an action. The current implementation is almost there except that the state tuple needs to augment with a list of additional delay variables. The reaction axioms should set these variables, and the Actions axioms should reference these additional delay variables.
[C] Support C time value macros (such as MS(100)).
[C] In TrafficLight.lf, if an action is visible, not using it blocks the model. So if one branch of an if statement is not using it, the entire model is blocked.
[State space] Detect Zeno behavior (zero delay cycle) during state space exploration. The current behavior seems to alternate between (0,0) and (0,1) (when running Election.lf).
[State space] One-off timer declarations that look like timer t(1 nsec) currently send the explorer into an infinite loop.
[Diagram] Render CEX diagrams.
[MTL] In the ADAS model, the property, ADASModel_l_reaction_0 ==> (F[0, 50 msec]( ADASModel_b_reaction_0 )), returns trivially true.
[MTL] The parsing of X() is sometimes problematic.

For logical time-based semantics:

Generate axioms for simultaneous reaction invocations while preserving reaction priorities.

Notes on maintaining this feature:

To develop the Uclid encoding, it is good to first develop a small example manually and then codify the axioms in the Uclid generator.

Debugging tips:

To debug the C AST, there is a handy function in AstUtils.java, printStackTraceAndMatchedText(), that can print the string matched by ANTLR as well as the stack trace of the visitor functions.
Unused triggers can block the model (producing trivially true).
Insufficient CT can block the model.

…being removed.

…ctions, and DSL-related things.

…n use.

cmnrd · 2023-07-13T12:28:32Z

The new setup for the verifier test works now. However, the tests revealed a problem in the generator:

 java.lang.AssertionError
    	at org.lflang.generator.ReactorInstance.<init>(ReactorInstance.java:96)
    	at org.lflang.ast.ASTUtils.createMainReactorInstance(ASTUtils.java:604)
    	at org.lflang.analyses.uclid.UclidGenerator.doGenerate(UclidGenerator.java:197)
    	at org.lflang.generator.LFGenerator.runVerifierIfPropertiesDetected(LFGenerator.java:182)
    	at org.lflang.generator.LFGenerator.doGenerate(LFGenerator.java:124)

This wasn't observed before, because assertions are only enabled during testing.

lsk567 · 2023-07-14T14:23:16Z

Coverage is back to 75%!

lhstrh · 2023-07-14T15:40:55Z

That's great news!

lhstrh · 2023-07-18T20:49:57Z

If I run lfc --verify without having the proper dependencies installed I get an NPE:

lfc: fatal error: Error running generator
java.lang.NullPointerException: Cannot invoke "org.lflang.util.LFCommand.run()" because "command" is null
        at org.lflang.analyses.uclid.UclidRunner.run(UclidRunner.java:175)
        at org.lflang.generator.LFGenerator.runVerifierIfPropertiesDetected(LFGenerator.java:198)
        at org.lflang.generator.LFGenerator.doGenerate(LFGenerator.java:124)
        at org.eclipse.xtext.generator.GeneratorDelegate.doGenerate(GeneratorDelegate.java:44)
        at org.eclipse.xtext.generator.GeneratorDelegate.generate(GeneratorDelegate.java:35)
        at org.lflang.cli.Lfc.invokeGenerator(Lfc.java:193)
        at org.lflang.cli.Lfc.doRun(Lfc.java:156)
        at org.lflang.cli.CliBase.run(CliBase.java:145)
        at picocli.CommandLine.executeUserObject(CommandLine.java:2026)
        at picocli.CommandLine.access$1500(CommandLine.java:148)
        at picocli.CommandLine$RunLast.executeUserObjectOfLastSubcommandWithSameParent(CommandLine.java:2461)
        at picocli.CommandLine$RunLast.handle(CommandLine.java:2453)
        at picocli.CommandLine$RunLast.handle(CommandLine.java:2415)
        at picocli.CommandLine$AbstractParseResultHandler.execute(CommandLine.java:2273)
        at picocli.CommandLine$RunLast.execute(CommandLine.java:2417)
        at picocli.CommandLine.execute(CommandLine.java:2170)
        at org.lflang.cli.CliBase.doExecute(CliBase.java:117)
        at org.lflang.cli.CliBase.cliMain(CliBase.java:109)
        at org.lflang.cli.Lfc.main(Lfc.java:143)
        at org.lflang.cli.Lfc.main(Lfc.java:133)

There should be a proper error message explaining what is missing.

Yes, this is a bug. I will fix it now.

Has this been fixed, @lsk567?

lhstrh

Looks good to me! Thanks for addressing the code coverage issue!

core/src/main/java/org/lflang/generator/LFGenerator.java

lsk567 · 2023-07-19T09:13:20Z

If I run lfc --verify without having the proper dependencies installed I get an NPE:

lfc: fatal error: Error running generator
java.lang.NullPointerException: Cannot invoke "org.lflang.util.LFCommand.run()" because "command" is null
        at org.lflang.analyses.uclid.UclidRunner.run(UclidRunner.java:175)
        at org.lflang.generator.LFGenerator.runVerifierIfPropertiesDetected(LFGenerator.java:198)
        at org.lflang.generator.LFGenerator.doGenerate(LFGenerator.java:124)
        at org.eclipse.xtext.generator.GeneratorDelegate.doGenerate(GeneratorDelegate.java:44)
        at org.eclipse.xtext.generator.GeneratorDelegate.generate(GeneratorDelegate.java:35)
        at org.lflang.cli.Lfc.invokeGenerator(Lfc.java:193)
        at org.lflang.cli.Lfc.doRun(Lfc.java:156)
        at org.lflang.cli.CliBase.run(CliBase.java:145)
        at picocli.CommandLine.executeUserObject(CommandLine.java:2026)
        at picocli.CommandLine.access$1500(CommandLine.java:148)
        at picocli.CommandLine$RunLast.executeUserObjectOfLastSubcommandWithSameParent(CommandLine.java:2461)
        at picocli.CommandLine$RunLast.handle(CommandLine.java:2453)
        at picocli.CommandLine$RunLast.handle(CommandLine.java:2415)
        at picocli.CommandLine$AbstractParseResultHandler.execute(CommandLine.java:2273)
        at picocli.CommandLine$RunLast.execute(CommandLine.java:2417)
        at picocli.CommandLine.execute(CommandLine.java:2170)
        at org.lflang.cli.CliBase.doExecute(CliBase.java:117)
        at org.lflang.cli.CliBase.cliMain(CliBase.java:109)
        at org.lflang.cli.Lfc.main(Lfc.java:143)
        at org.lflang.cli.Lfc.main(Lfc.java:133)

There should be a proper error message explaining what is missing.

Yes, this is a bug. I will fix it now.

Has this been fixed, @lsk567?

Yes, this has been fixed. Now, if any of the dependencies is not found when running lfc with the --verify flag, an error is printed.

lfc: info: Generating code for: file:/Users/shaokai/git/lingua-franca/test/C/src/verifier/ADASModel.lf
lfc: info: Generation mode: STANDALONE
lfc: info: Generating sources into: /Users/shaokai/git/lingua-franca/test/C/src-gen/verifier/ADASModel
lfc: error: Fail to check the generated verification models because Uclid5 or Z3 is not installed.
lfc: fatal error: Aborting due to 1 previous error.

> Task :cli:lfc:run FAILED

FAILURE: Build failed with an exception.

lhstrh · 2023-07-19T22:14:49Z

The only thing preventing this from getting merged is lf-lang/epoch#19.

lsk567 · 2023-07-20T09:55:51Z

The only thing preventing this from getting merged is lf-lang/epoch#19.

Yes, I am working on it. I also consulted @a-sr for help on this. It will probably take some extra time.

cmnrd

I haven't done a careful code review, but I am Ok with merging this as soon as we have a strategy for fixing lf-lang/epoch#19.

lsk567 · 2023-07-24T21:01:33Z

lf-lang/epoch#19 is now ready to go. All credits go to @a-sr! I think we should merge this PR (#1271 ) first, since epoch depends on it?

cmnrd · 2023-09-27T11:32:54Z

core/src/main/java/org/lflang/generator/LFGenerator.java

+      cleanIfNeeded(lfContext);
+
+      // If @property annotations are used, run the LF verifier.
+      runVerifierIfPropertiesDetected(resource, lfContext);


Is there a reason for calling the verifier here instead of in GeneratorBase?

I spend some time today wondering why the verifier tests pass on my machine, although I don't have uclid installed. Turns out that the errors reported by the verifier are ignored, because the message reporter is reset at the beginning of doGenerate() in GeneratorBase. So it seems like the verifier should be called in GeneratorBase, after cleaning and resetting the message reporter.

At the time when I implemented this, it felt a bit more natural to call the verifier outside of GeneratorBase, because it focuses on generating target source code.

But I am certainly not against moving it into GeneratorBase. :-)

lsk567 added 30 commits November 21, 2022 16:57

Begin the Java port of the UclidGenerator

f03bf86

Do some more porting

905bbcc

Finish generating traces

e8fe270

Minor fixes

b09633f

Start to generate reaction and state variable declarations

9a73349

Ensure that when building the reaction instance graph, nodes are not …

7b31537

…being removed.

Generate state variables and triggers

f3d9cc8

Generate up to reactor semantics

21d1718

Generate runner script and refactor a few things. TODO: Triggers, rea…

c5bc411

…ctions, and DSL-related things.

Uclid bug fixes

d704e51

Start to generate reactions and triggers

7e1a726

Continue generating reactions

f3a54c6

Start populating state variables and triggers

5d8d9a4

Keep generating lists

c2bccb5

Remove dead code

7bba94a

Finish generating actions

1e8e401

Deprecate reaction instance graph

49d11e3

Generate connections

646ba72

Bug fix

13db2db

Start a C subset target

60c5700

Remove the super.doGenerate() call.

8baa668

Remove the new target. Invoke the uclid generator when @Property is i…

faa5203

…n use.

Add an instance class for state variables

7d79196

Add Antlr4 to the gradle project

f194a01

Move Antlr grammar

7c9274c

Fix Antlr generated file location, start MTL transpiler

301ed16

Start to generate properties based on property attributes

52040d0

Use the MTLParser to generate parse trees

21efab8

Update syntax to include expressions

38a31ff

Start to transpile MTL using a visitor

47ab696

cmnrd and others added 7 commits July 12, 2023 17:09

add verifier test class

4b83bcf

exclude the verifier tests from zephyr and multithreaded

4db4404

update CI

c9f80aa

ensure correct directory

2747157

Output error message when dependencies are not installed.

d07e029

actually ensure correct directory

06a8944

bring workflow up to standard and add debug info

4696ee0

lsk567 added 2 commits July 13, 2023 17:32

Fix the assertion error.

ad4daeb

Adjust platform and test level

2e7cfb0

lhstrh requested a review from cmnrd July 18, 2023 20:50

lhstrh approved these changes Jul 18, 2023

View reviewed changes

core/src/main/java/org/lflang/generator/LFGenerator.java Outdated Show resolved Hide resolved

Update core/src/main/java/org/lflang/generator/LFGenerator.java

d87763f

lsk567 and others added 2 commits July 19, 2023 11:14

Merge branch 'master' into verifier

5a13524

Apply spotless

35f0887

cmnrd approved these changes Jul 20, 2023

View reviewed changes

a-sr mentioned this pull request Jul 22, 2023

Uclid5-based LF Verifier lf-lang/epoch#26

Merged

lhstrh added this pull request to the merge queue Jul 25, 2023

Merged via the queue into master with commit 9776309 Jul 25, 2023
43 checks passed

lhstrh deleted the verifier branch July 25, 2023 07:42

petervdonovan added the feature New feature label Aug 26, 2023

cmnrd reviewed Sep 27, 2023

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uclid5-based LF Verifier #1271

Uclid5-based LF Verifier #1271

lsk567 commented Jul 3, 2022 •

edited

Loading

cmnrd commented Jul 13, 2023

lsk567 commented Jul 14, 2023

lhstrh commented Jul 14, 2023

lhstrh commented Jul 18, 2023

lhstrh left a comment

lsk567 commented Jul 19, 2023

lhstrh commented Jul 19, 2023

lsk567 commented Jul 20, 2023

cmnrd left a comment

lsk567 commented Jul 24, 2023

cmnrd Sep 27, 2023

lsk567 Sep 27, 2023

Uclid5-based LF Verifier #1271

Uclid5-based LF Verifier #1271

Conversation

lsk567 commented Jul 3, 2022 • edited Loading

cmnrd commented Jul 13, 2023

lsk567 commented Jul 14, 2023

lhstrh commented Jul 14, 2023

lhstrh commented Jul 18, 2023

lhstrh left a comment

Choose a reason for hiding this comment

lsk567 commented Jul 19, 2023

lhstrh commented Jul 19, 2023

lsk567 commented Jul 20, 2023

cmnrd left a comment

Choose a reason for hiding this comment

lsk567 commented Jul 24, 2023

cmnrd Sep 27, 2023

Choose a reason for hiding this comment

lsk567 Sep 27, 2023

Choose a reason for hiding this comment

lsk567 commented Jul 3, 2022 •

edited

Loading