Smoke Testing #211
Smoke Testing #211
Conversation
…ement at the specifed line number.
…k; remove short command line option for smoke testing.
src/main/scala/uclid/UclidMain.scala
Outdated
| @@ -47,6 +47,8 @@ import scala.collection.immutable._ | |||
| import lang.{Identifier, Module, _} | |||
| import uclid.Utils.ParserErrorList | |||
| import com.typesafe.scalalogging.Logger | |||
| import java.io.{File, FileWriter} | |||
There was a problem hiding this comment.
Do we need this import?
There was a problem hiding this comment.
No. It was left over from my first attempt at smoke testing (where I rewrote the file); I removed it now.
| val file = scala.io.Source.fromFile(srcFile) | ||
| // TODO: parse line by line instead of loading the complete file into a string |
There was a problem hiding this comment.
don't delete this todo please
There was a problem hiding this comment.
My bad, I must have deleted it by accident! It's back in its rightful place now :D
src/main/scala/uclid/UclidMain.scala
Outdated
| @@ -432,6 +446,12 @@ object UclidMain { | |||
| passManager.addPass(new ModuleEliminator(mainModuleName)) | |||
| // Expands (grounds) finite_forall and finite_exists quantifiers | |||
| passManager.addPass(new FiniteQuantsExpander()) | |||
| // test unreachable code | |||
There was a problem hiding this comment.
Is there an argument for putting this here? Would it be better to put it before all the passes? after?
There was a problem hiding this comment.
Yes and no. I moved it there because the LTL specification check was originally part of SmokeRemover, and it would not work when the passes were in that part of the code. Now that we have the SmokeAnalyzer pass to perform the checks, it works just fine (and it is a lot faster). I moved this block of code to the top of createCompilePassManager again.
| package uclid | ||
| package lang | ||
|
|
||
| class SmokeAnalyzePass extends RewritePass { |
There was a problem hiding this comment.
If you're doing an analysis use the analysis pass class, not the rewrite pass class. More efficient.
|
It looks mostly good! I added some comments that I'd like you to address but then I think I'm happy with it. Also, maybe it is worth adding an example/test. I'm not sure exactly what the test would look like though. @polgreen what do you think? |
There was a problem hiding this comment.
I'll take a look again once you've fixed Federico's comments, but overall looks good, but it definitely needs tests.
Tests should:
- check that it's identifying the correct number of reachable/unreachable lines of code correctly for a few different configurations of UCLID files (what does it do if it has multiple modules? Does it only do the main module? Does it do all the modules? Does it work for inlined procedures? What about not-inlined procedures? Check that it works correctly with assumptions as well as with )
- check that the error message for LTL is correctly thrown
A question:
- Does it remove pre/post conditions? Because those can result in things being unreachable if we do no-inlining of procedures, because we generate an "assume post condition" after the point where the procedure was called. So you might not be getting correct results for those cases if you are removing the pre/post conditions before we no-inline the procedures
|
is this ready for review again? |
|
This looks mostly good to me! I don't know about introducing the shell files for installations (I'm fine with doing it but not sure this pull request is the right place for that). The tests look good too but are not in the CI. I think that is fine too, though. @polgreen are we good to merge? |
|
Can you make the tests run in the CI before you merge, please? And then it's good to merge. We tend to break things that don't get tested by the CI |
…hat CI uses same code as main source.
|
I added SmokeSpec to the CI. Tests pass. I think we should merge. |
Check for unreachable code by running uclid with the --smoke flag.