Leiqi concrete simulator #260
Conversation
lichye
force-pushed
the
leiqi-concreteSimulator
branch
2 times, most recently
from
a816b70 to
d8c1f73
Compare
add autotester fix up bugs
add setup sbt
lichye
force-pushed
the
leiqi-concreteSimulator
branch
from
95353a9 to
6cd8952
Compare
There was a problem hiding this comment.
Looks good. I have some questions about the comments that have been left in, and specifically what is a ConcreteUndef, and when do we encounter this.
Also, please add tests for
- all configuration options of the simulator
- testing violated assertions
- testing assumptions
- printing the trace
| var varMap: scala.collection.mutable.Map[Identifier, ConcreteValue] = collection.mutable.Map(); | ||
| var varTypeMap: scala.collection.mutable.Map[Identifier, Type] = collection.mutable.Map(); | ||
| //var functionMap: scala.collection.mutable.Map[Identifier, ConcreteValue] = collection.mutable.Map(); | ||
| var inputMap: scala.collection.mutable.Map[Identifier, ConcreteValue] = collection.mutable.Map(); |
There was a problem hiding this comment.
Is the functionMap no longer needed? If so, can you delete this commented out line please
There was a problem hiding this comment.
It was in the todo list. So, I left the function Map here.
| sealed abstract class ConcreteValue{ | ||
| def valueClone: ConcreteValue; | ||
| } | ||
| case class ConcreteUndef () extends ConcreteValue{ |
There was a problem hiding this comment.
What is an Undef? Could you add a comment above this saying what it is? (The others are all obvious)
|
|
||
| object ConcreteSimulator { | ||
| //debug useful flag | ||
| var isPrintResult: Boolean = true; |
There was a problem hiding this comment.
debug printing should go via a logger (see the logger in symbolic simulator:
)There was a problem hiding this comment.
Or you can use UclidMain.printError, UclidMain.printStatus etc
| def write (variable: Identifier, value: ConcreteValue) { | ||
| if (varMap.contains(variable)) varMap(variable) = value | ||
| else if (inputMap.contains(variable)) inputMap(variable) = value | ||
| // else throw new Error(f"Variable ${variable.toString} not found in context") |
There was a problem hiding this comment.
Should we still be throwing this error?
| } | ||
| // TODO: ... fill in | ||
| case ArrayType(inType, outType) => { | ||
| // TODO: outType could be complex type like another array or record |
There was a problem hiding this comment.
Is this TODO still relevant? If not, can you delete it
| new smt.SynthLibInterface(config.synthesizer, config.sygusFormat) | ||
| val isConcrete = config.simulate && module.cmds.exists(p => p.name.toString == "concrete") | ||
| if (isConcrete) { | ||
| UclidMain.printVerbose("Begining Concrete Simulation") |
| property jump_a: a!=3; | ||
|
|
||
| control { | ||
| v = bmc(5); |
There was a problem hiding this comment.
this test does bmc, not concrete
| @@ -113,6 +114,10 @@ object UclidMain { | |||
| (exec, c) => c.copy(synthesizer = exec.split(" ").toList) | |||
| }.text("Command line to invoke SyGuS synthesizer.") | |||
|
|
|||
| opt[String]('c', "simulate").valueName("<Cmd>").action{ | |||
There was a problem hiding this comment.
So to use this, we have to use simulate and the command "concrete" in the control block? What happens if i use simulate without the command "concrete" in the control block?
| control { | ||
| v = concrete (5); | ||
| check; | ||
| // v.print_concrete_trace(a,numbers); |
There was a problem hiding this comment.
none of your tests actually run print_concrete_trace.
| ConcreteSpec.expectedFails("./test/concrete/concrete-9.ucl", 1) | ||
| } | ||
| "concrete-10.ucl" should "fail one assertion." in { | ||
| ConcreteSpec.expectedFails("./test/concrete/concrete-10.ucl", 1) |
There was a problem hiding this comment.
Could you add a test that prints the concrete trace, and checks the length of it at least (there are some tests in VerifierSpec that do this that you can copy).
Also make sure at least one test runs each of the configuration options
Also, test what should happen if an assertion is violated by the concrete trace
And test that assumptions block the concrete values correctly
This pull request will merge the concrete engine into the master respority.
The code does not change the main work flow of the Uclid5.
When "-c" is called, we will run concrete Simulator to simulate the uclid file.
There is still lots of util to be supported , but a early version will be helpful for testing.