From 468b9dc400b30c09f9179d3e3aeaae2dff6501fb Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Fri, 6 Feb 2015 19:32:16 +0100
Subject: [PATCH] Fix bug that misses tests
---
.../leon/repair/RepairTrackingEvaluator.scala | 25 +++++++++++++++----
1 file changed, 20 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
index 8ac452b9f..c0156a9e2 100644
--- a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
@@ -8,6 +8,7 @@ import leon.purescala.TypeTrees._
import leon.purescala.Definitions._
import leon.LeonContext
import leon.evaluators.RecursiveEvaluator
+import leon.synthesis._
class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog, 50000) {
type RC = CollectingRecContext
@@ -21,13 +22,25 @@ class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends Recursive
// This is a call graph to track dependencies of function invocations.
// If fi1 calls fi2 but fails fi2's precondition, we consider it
// fi1's fault and we don't register the dependency.
- private val callGraph : MMap[FI, Set[FI]] = MMap().withDefaultValue(Set())
+ private val callGraph : MMap[FI, Set[FI]] = MMap()//.withDefaultValue(Set())
+ private def registerNode(fi : FI) = if (!callGraph.contains(fi)) callGraph update (fi, Set())
private def registerCall(fi : FI, lastFI : Option[FI]) = {
lastFI foreach { lfi =>
callGraph update (lfi, callGraph(lfi) + fi)
}
}
- def fullCallGraph = leon.utils.GraphOps.transitiveClosure(callGraph.toMap)
+ def fullCallGraph = {
+ /*println("About to print")
+ for{
+ (test, tests) <-callGraph
+
+ } {
+ println(test._2 mkString ", ")
+ println(new ExamplesTable("", tests.toSeq.map{ x => InExample(x._2)}).toString)
+ }*/
+
+ leon.utils.GraphOps.transitiveClosure(callGraph.toMap)
+ }
// Tracks if every function invocation succeeded or failed
private val fiStatus_ : MMap[FI, Boolean] = MMap().withDefaultValue(false)
@@ -48,9 +61,6 @@ class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends Recursive
gctx.stepsLeft -= 1
val evArgs = args.map(a => e(a))
-
- // We consider this function invocation successful, unless the opposite is proven.
- registerSuccessful(tfd.fd, evArgs)
// build a mapping for the function...
val frameBlamingCaller = rctx.withVars((tfd.params.map(_.id) zip evArgs).toMap)
@@ -58,8 +68,11 @@ class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends Recursive
if(tfd.hasPrecondition) {
e(tfd.precondition.get)(frameBlamingCaller, gctx) match {
case BooleanLiteral(true) =>
+ // We consider this function invocation successful, unless the opposite is proven.
+ registerSuccessful(tfd.fd, evArgs)
// Only register a call dependency if the call we depend on does not fail precondition
registerCall((tfd.fd, evArgs), rctx.lastFI)
+ registerNode((tfd.fd, evArgs))
case BooleanLiteral(false) =>
// Caller's fault!
rctx.lastFI foreach registerFailed
@@ -70,6 +83,8 @@ class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends Recursive
throw RuntimeError(typeErrorMsg(other, BooleanType))
}
} else {
+ registerSuccessful(tfd.fd, evArgs)
+ registerNode((tfd.fd, evArgs))
registerCall((tfd.fd, evArgs), rctx.lastFI)
}
--
GitLab