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.

Sign up for GitHub

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

Jump to bottom

Update traceInduct and clustering #1052

Merged
merged 6 commits into from
May 20, 2021
Merged

Update traceInduct and clustering #1052

merged 6 commits into from
May 20, 2021

Conversation

drganam
Copy link
Collaborator

@drganam drganam commented May 14, 2021 •
edited
Loading

Reimplements #931 using .holds instead of ensuring, and using the new BodyWithSpecs API

@drganam drganam mentioned this pull request May 14, 2021
Open
@vkuncak vkuncak requested a review from jad-hamza May 19, 2021 09:28
jad-hamza
jad-hamza approved these changes May 19, 2021
View reviewed changes
Copy link
Contributor

@jad-hamza jad-hamza left a comment

Choose a reason for hiding this comment

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

I had a quick look and it looks good to me! Should you maybe add positions to the functions/lemmas you're adding?

core/src/main/scala/stainless/extraction/trace/Trace.scala Outdated
case Precondition(cond) => Precondition(exprOps.replaceFromSymbols(specsMap, cond)).setPos(spec)
case LetInSpec(vd, expr) => LetInSpec(vd, exprOps.replaceFromSymbols(specsMap, expr)).setPos(spec)
case Measure(measure) => Measure(exprOps.replaceFromSymbols(specsMap, measure)).setPos(spec)
case s => s
Copy link
Contributor

Choose a reason for hiding this comment

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

Maybe add a crash in this last case to make sure we modify that if we ever add new specs.

core/src/main/scala/stainless/extraction/trace/Trace.scala Outdated
}

}
private def shouldBeChecked(fid: Identifier): Boolean = pathsOpt match {
Copy link
Contributor

Choose a reason for hiding this comment

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

Can you refactor this to use the already existing shouldBeChecked?

core/src/main/scala/stainless/frontend/BatchedCallBack.scala Outdated
report = Report(reports)
rerunPipeline = Trace.nextIteration(report)
if (!rerunPipeline) Trace.printEverything
//else report.emit(context)
Copy link
Contributor

Choose a reason for hiding this comment

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

Extra comment

core/src/main/scala/stainless/MainHelpers.scala Outdated
@@ -166,6 +168,11 @@ trait MainHelpers extends inox.MainHelpers { self =>

import ctx.{ reporter, timers }

if (extraction.trace.Trace.optionsError) {
reporter.error(s"Equivalence checking for --comparefuns and --models only works in batched mode.")
System.exit(1)
Copy link
Contributor

Choose a reason for hiding this comment

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

You can use reporter.fatalError() to crash instead of reporter.error() followed by System.exit(1).

Copy link
Contributor

Choose a reason for hiding this comment

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

Thanks for the fixes! I think you can remove System.exit(1) when you use fatalError.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Oops I forgot to remove it, thanks!

@drganam drganam force-pushed the trace-ensuring-newspecs branch from bbf73eb to 2e03319 Compare May 20, 2021 13:33
@jad-hamza
Copy link
Contributor

GenCSuite uses runMainWithArgs:

stainless/frontends/scalac/src/it/scala/stainless/Utils.scala

Lines 12 to 20 in a0a3ff8

def runMainWithArgs(args: Array[String]) = {
val ctx = Main.setup(args).copy(reporter = new inox.TestSilentReporter())
val compilerArgs = args.toList filterNot { _.startsWith("--") }
var compiler = frontend.build(ctx, compilerArgs, stainless.Main.factory)
ctx.reporter.info(s"Running: stainless ${args.mkString(" ")}")
compiler.run()
compiler.join()
compiler.getReport
}

Is there a problem of initialisation for the trace induct phase?

@drganam drganam force-pushed the trace-ensuring-newspecs branch from 2cab6b1 to 4a99dae Compare May 20, 2021 15:06
@drganam
Copy link
Collaborator Author

drganam commented May 20, 2021

@jad-hamza not sure what was it with GenCSuite, this time larabot says SMTZ3TypeCheckerSuite is failing

@jad-hamza
Copy link
Contributor

I hope the example that failed in SMTZ3TypeCheckerSuite was just due to unstability?
GenCSuite didn't run in the latest build because it was removed from larabot.conf (you need to rebase on master for it to run).

For GenCSuite, according to http://laraquad4.epfl.ch:9000/epfl-lara/stainless/build/679/3405, the exception is thrown on the get here:
https://github.com/drganam/stainless/blob/4a99daeeb63e5b2bda471d648f58efc58786349c/core/src/main/scala/stainless/extraction/trace/Trace.scala#L397

@drganam
Copy link
Collaborator Author

drganam commented May 20, 2021

Makes sense, let's see if it's ok now

@jad-hamza
Copy link
Contributor

Very good, thanks!

@jad-hamza jad-hamza merged commit 73684b3 into epfl-lara:master May 20, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jad-hamza jad-hamza jad-hamza approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@drganam @jad-hamza