Skip to content
Snippets Groups Projects
Commit 16e93516 authored by Philippe Suter's avatar Philippe Suter
Browse files

Changed some options (--CAV doesn't exist anymore and is on by default). New...

Changed some options (--CAV doesn't exist anymore and is on by default). New option --quickcheck uses Régis parrallel and random solvers.

parent f78e89b5
No related branches found
No related tags found
No related merge requests found
...@@ -27,17 +27,16 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog ...@@ -27,17 +27,16 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
" -P:funcheck:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" + " -P:funcheck:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
" -P:funcheck:axioms Generate simple forall axioms for recursive functions when possible" + "\n" + " -P:funcheck:axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
" -P:funcheck:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" + " -P:funcheck:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
" -P:funcheck:nobapa Disable BAPA Z3 extension" + "\n" + " -P:funcheck:bapa Use BAPA Z3 extension (incompatible with many other things)" + "\n" +
" -P:funcheck:impure Generate testcases only for impure functions" + "\n" + " -P:funcheck:impure Generate testcases only for impure functions" + "\n" +
" -P:funcheck:testcases=[1,2] Number of testcases to generate per function" + "\n" + " -P:funcheck:testcases=[1,2] Number of testcases to generate per function" + "\n" +
" -P:funcheck:testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" + " -P:funcheck:testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
" -P:funcheck:timeout=N Sets a timeout of N seconds (FairZ3 only)" + "\n" + " -P:funcheck:timeout=N Sets a timeout of N seconds" + "\n" +
" -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" + " -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
" -P:funcheck:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" + " -P:funcheck:prune Use additional SMT queries to rule out some unrollings" + "\n" +
" -P:funcheck:CAV CAV 2011 settings. In progress." + "\n" + " -P:funcheck:cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
" -P:funcheck:prune (with CAV) Use additional SMT queries to rule out some unrollings." + "\n" + " -P:funcheck:quickcheck Use QuickCheck-like random search in parrallel with Z3" + "\n" +
" -P:funcheck:cores (with CAV) Use UNSAT cores in the unrolling/refinement step." + "\n" + " -P:funcheck:noLuckyTests Do not perform additional tests to potentially find models early"
" -P:funcheck:noLuckyTests (with CAV) Do not perform additional tests to potentially find models early."
) )
/** Processes the command-line options. */ /** Processes the command-line options. */
...@@ -51,14 +50,12 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog ...@@ -51,14 +50,12 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
case "tolerant" => silentlyTolerateNonPureBodies = true case "tolerant" => silentlyTolerateNonPureBodies = true
case "nodefaults" => purescala.Settings.runDefaultExtensions = false case "nodefaults" => purescala.Settings.runDefaultExtensions = false
case "axioms" => purescala.Settings.noForallAxioms = false case "axioms" => purescala.Settings.noForallAxioms = false
case "nobapa" => purescala.Settings.useBAPA = false case "bapa" => purescala.Settings.useBAPA = true
case "impure" => purescala.Settings.impureTestcases = true case "impure" => purescala.Settings.impureTestcases = true
case "newPM" => { println("''newPM'' is no longer a command-line option, because the new translation is now on by default."); System.exit(0) }
case "XP" => purescala.Settings.experimental = true case "XP" => purescala.Settings.experimental = true
case "PLDI" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = true; purescala.Settings.useFairInstantiator = false; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
case "CAV" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = false; purescala.Settings.useFairInstantiator = true; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
case "prune" => purescala.Settings.pruneBranches = true case "prune" => purescala.Settings.pruneBranches = true
case "cores" => purescala.Settings.useCores = true case "cores" => purescala.Settings.useCores = true
case "quickcheck" => purescala.Settings.useQuickCheck = true
case "noLuckyTests" => purescala.Settings.luckyTest = false case "noLuckyTests" => purescala.Settings.luckyTest = false
case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 } case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*) case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
......
...@@ -83,15 +83,19 @@ object Extensions { ...@@ -83,15 +83,19 @@ object Extensions {
} }
// these extensions are always loaded, unless specified otherwise // these extensions are always loaded, unless specified otherwise
val defaultExtensions: Seq[Extension] = if(Settings.runDefaultExtensions) { val defaultExtensions: Seq[Extension] = if(Settings.runDefaultExtensions) {
//(new TestExtension(extensionsReporter)) :: val z3s : Solver = (if(Settings.useFairInstantiator) {
//new RandomSolver(extensionsReporter, Some(50)) ::
//new ParallelSolver(extensionsReporter, new RandomSolver(extensionsReporter), new FairZ3Solver(extensionsReporter)) ::
(if(Settings.useFairInstantiator) {
(new FairZ3Solver(extensionsReporter)) (new FairZ3Solver(extensionsReporter))
} else { } else {
(new Z3Solver(extensionsReporter)) (new Z3Solver(extensionsReporter))
}) :: })
Nil
val qcs : Solver = (if(Settings.useQuickCheck) {
new ParallelSolver(extensionsReporter, new RandomSolver(extensionsReporter), z3s)
} else {
z3s
})
qcs :: Nil
} else { } else {
Nil Nil
} }
......
...@@ -24,8 +24,9 @@ class ParallelSolver(reporter: Reporter, solvers: Solver*) extends Solver(report ...@@ -24,8 +24,9 @@ class ParallelSolver(reporter: Reporter, solvers: Solver*) extends Solver(report
solvers.foreach(_.setProgram(prog)) solvers.foreach(_.setProgram(prog))
} }
val description = "Solver running subsolvers in parallel" val description = "Solver running subsolvers in parallel " + solvers.map(_.description).mkString("(", ", ", ")")
override val shortDescription = "parallel" override val shortDescription = solvers.map(_.shortDescription).mkString("//")
override val superseeds : Seq[String] = solvers.map(_.shortDescription).toSeq
private val lock = new Lock private val lock = new Lock
private var nbResponses: Int = 0 private var nbResponses: Int = 0
......
...@@ -63,7 +63,7 @@ class RandomSolver(reporter: Reporter, val nbTrial: Option[Int] = None) extends ...@@ -63,7 +63,7 @@ class RandomSolver(reporter: Reporter, val nbTrial: Option[Int] = None) extends
private var running = true private var running = true
def solve(expression: Expr) : Option[Boolean] = { def solve(expression: Expr) : Option[Boolean] = {
println("solving: " + expression) //println("solving: " + expression)
val vars = variablesOf(expression) val vars = variablesOf(expression)
val randomValue = randomValueGen() val randomValue = randomValueGen()
running = true running = true
...@@ -80,7 +80,7 @@ class RandomSolver(reporter: Reporter, val nbTrial: Option[Int] = None) extends ...@@ -80,7 +80,7 @@ class RandomSolver(reporter: Reporter, val nbTrial: Option[Int] = None) extends
val var2val: Map[Identifier, Expr] = Map(vars.map(v => (v, randomValue(v.getType))).toList: _*) val var2val: Map[Identifier, Expr] = Map(vars.map(v => (v, randomValue(v.getType))).toList: _*)
println("trying with : " + var2val) //println("trying with : " + var2val)
val evalResult = eval(var2val, expression, None) val evalResult = eval(var2val, expression, None)
evalResult match { evalResult match {
......
...@@ -11,15 +11,16 @@ object Settings { ...@@ -11,15 +11,16 @@ object Settings {
var noForallAxioms: Boolean = true var noForallAxioms: Boolean = true
var unrollingLevel: Int = 0 var unrollingLevel: Int = 0
var zeroInlining : Boolean = false var zeroInlining : Boolean = false
var useBAPA: Boolean = true var useBAPA: Boolean = false
var impureTestcases: Boolean = false var impureTestcases: Boolean = false
var nbTestcases: Int = 1 var nbTestcases: Int = 1
var testBounds: (Int, Int) = (0, 3) var testBounds: (Int, Int) = (0, 3)
var useInstantiator: Boolean = false var useInstantiator: Boolean = false
var useFairInstantiator: Boolean = false var useFairInstantiator: Boolean = true
var useCores : Boolean = false var useCores : Boolean = false
var pruneBranches : Boolean = false var pruneBranches : Boolean = false
def useAnyInstantiator : Boolean = useInstantiator || useFairInstantiator def useAnyInstantiator : Boolean = useInstantiator || useFairInstantiator
var solverTimeout : Option[Int] = None var solverTimeout : Option[Int] = None
var luckyTest : Boolean = true var luckyTest : Boolean = true
var useQuickCheck : Boolean = false
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment