Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Uclid5-based LF Verifier #1271

Merged
merged 189 commits into from
Jul 25, 2023
Merged

Uclid5-based LF Verifier #1271

merged 189 commits into from
Jul 25, 2023

Conversation

lsk567
Copy link
Collaborator

@lsk567 lsk567 commented Jul 3, 2022

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:

  • Implement an MTL parser that parses user-specified properties. Generate uclid axioms that correspond to the MTL properties.
  • Implement a C parser and generate uclid axioms (or smt-lib directly) from analyzable C fragments.
  • Automatically calculate the completeness threshold for an MTL property.
  • Support timers.
  • Speed up SMT file generation process.
  • Generate a .dot file for the state space diagram.
  • Support lf_schedule_int call (which takes 3 params).
  • [CEX] Parse negative numbers and a let binding from a counterexample.
  • A regression test suite and a CI workflow for the LF verifier, so that we know that adding a new feature would not break others (axioms are fairly delicate and might interfere with each other).
  • Trim the test cases so that they can be run on a machine with 7G RAM.
  • [State space] The event queue needs to sort events by name in addition to time.
  • Show a warning for "experimental feature".
  • Check for uclid and z3.

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:

  1. 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:

  1. 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.
  2. Unused triggers can block the model (producing trivially true).
  3. Insufficient CT can block the model.

@cmnrd
Copy link
Collaborator

cmnrd commented Jul 13, 2023

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
Copy link
Collaborator Author

lsk567 commented Jul 14, 2023

Coverage is back to 75%!

@lhstrh
Copy link
Member

lhstrh commented Jul 14, 2023

That's great news!

@lhstrh
Copy link
Member

lhstrh commented Jul 18, 2023

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 lhstrh requested a review from cmnrd July 18, 2023 20:50
Copy link
Member

@lhstrh lhstrh left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

core/src/main/java/org/lflang/generator/LFGenerator.java Outdated Show resolved Hide resolved
@lsk567
Copy link
Collaborator Author

lsk567 commented Jul 19, 2023

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
Copy link
Member

lhstrh commented Jul 19, 2023

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

@lsk567
Copy link
Collaborator Author

lsk567 commented Jul 20, 2023

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.

Copy link
Collaborator

@cmnrd cmnrd left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Collaborator Author

lsk567 commented Jul 24, 2023

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?

@lhstrh lhstrh added this pull request to the merge queue Jul 25, 2023
Merged via the queue into master with commit 9776309 Jul 25, 2023
@lhstrh lhstrh deleted the verifier branch July 25, 2023 07:42
@petervdonovan petervdonovan added the feature New feature label Aug 26, 2023
cleanIfNeeded(lfContext);

// If @property annotations are used, run the LF verifier.
runVerifierIfPropertiesDetected(resource, lfContext);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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. :-)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature New feature
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants