Skip to content

Commit

Permalink
Some simplifications
Browse files Browse the repository at this point in the history
  • Loading branch information
@GSAir
GSAir committed Aug 6, 2019
1 parent 9541563 commit 36146b9
Show file tree
Hide file tree
Showing 13 changed files with 31 additions and 19 deletions.
9 changes: 8 additions & 1 deletion src/main/scala/CFrontend3.scala
View file
Expand Up @@ -671,7 +671,12 @@ trait CFGtoEngine extends CtoCFG with Approx with Omega {
key -> (if (isBool(key)) simplifyBool(value) else simplify(value))
}) // FIXME ???
case IR.Def(DUpdate(x, f, y)) => IR.update(simplify(x), simplify(f), simplify(y))
case r@IR.Def(DSelect(`randKey`, f)) => IR.select(randKey, simplify(f))
case x@IR.Def(DSelect(`randKey`, f)) =>
if (alwaysFalse(IR.not(IR.equal(x, IR.const(0))))) { // FIXME: hack if GRef(x) == 0
println(s"Simplifed ${IR.termToString(x)} to 0"); IR.const(0)
} else if (alwaysFalse(IR.not(IR.equal(x, IR.const(1))))) {
println(s"Simplifed ${IR.termToString(x)} to 1"); IR.const(1)
} else IR.select(randKey, simplify(f))
case IR.Def(DSelect(x, f)) => IR.select(simplify(x), simplify(f))
// (x26? * rand?((&rand:1,top))) + (x26? * (rand?((&rand:0,top)) * -1))
case IR.Def(DPlus(IR.Def(DTimes(a, b)), IR.Def(DTimes(a1, IR.Def(DTimes(b1, k: GConst)))))) if a == a1 && alwaysFalse(IR.not(IR.equal(b, b1))) => IR.times(a, IR.times(b, IR.plus(IR.const(1), k)))
Expand All @@ -697,6 +702,8 @@ trait CFGtoEngine extends CtoCFG with Approx with Omega {
case x@GRef(_) =>
if (alwaysFalse(IR.not(IR.equal(x, IR.const(0))))) { // FIXME: hack if GRef(x) == 0
println(s"Simplifed $x to 0"); IR.const(0)
} else if (alwaysFalse(IR.not(IR.equal(x, IR.const(1))))) {
println(s"Simplifed $x to 1"); IR.const(1)
} else {
x
}
Expand Down
3 changes: 1 addition & 2 deletions src/main/scala/Engine.scala
View file
Expand Up @@ -1192,12 +1192,11 @@ import java.io.{PrintStream,File,FileInputStream,FileOutputStream,FileNotFoundEx
case k => (k, lub(select(a,k),select(b0,k),select(b1,k))(mkey(fsym,k),n0))
}
(map(m.map(kv=>(kv._1,kv._2._1)).toMap), map(m.map(kv=>(kv._1,kv._2._2)).toMap))
case (_: GConst, _, GConst(b)) if subst(b0, n0, const(1)) == b1 =>
case (_: GConst, _, GConst(b)) if subst(b0, n0, const(1)) == b1 && subst(b0, n0, const(0)) == a => // special case
IRD.printTerm(a)
IRD.printTerm(b0)
IRD.printTerm(b1)
(b1, b1)
???
case (a,b0, Def(DUpdate(bX, `n0`, y))) if bX == b0 || (bX == map(Map()) && b0 == GError) => // array creation
//use real index var !!
val nX = mkey(fsym,n0)
Expand Down
12 changes: 8 additions & 4 deletions src/main/scala/Main.scala
View file
Expand Up @@ -273,13 +273,17 @@ object MyMain extends CFGtoEngine with Omega {
def constant(it: Int) = s"""
int main() {
int k, i;
int n = __VERIFIER_nondet_int();
k = 4;
i = 0;
while (i < $it) {
k = 9;
while (i < n) {
if (k <= 4) {
k = 9;
} else {
k += 1;
}
i = i + 1;
}
__VERIFIER_assert(($it > 0 && k == 9) || ($it == 0 && k == 4));
return 0;
}
"""
Expand Down Expand Up @@ -469,6 +473,6 @@ int main(void) {


def main(arr: Array[String]) = {
analyze(sin2) // constant(arr(0).toInt))
analyze(constant(arr(0).toInt))
}
}
4 changes: 2 additions & 2 deletions test-out/sv-bench/loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i.check
View file
Expand Up @@ -45,7 +45,7 @@
Final store:
{ "&i" -> [ if ((0 < r?((&r:0,top)))) { {
if ((0 < r?((&r:2,top)))) { {
if (((r?((&r:1,top)) + (r?((&r:0,top)) * -1)) < (r?((&r:2,top)) * 2))) { <error> } else { fixindex { x47? => if ((x47? < r?((&r:2,top)))) { (r?((&r:0,top)) < (r?((&r:1,top)) + -2)) } else { 0 } } }
if (((r?((&r:1,top)) + (r?((&r:0,top)) * -1)) < (r?((&r:2,top)) * 2))) { <error> } else { fixindex { x59? => if ((x59? < r?((&r:2,top)))) { (r?((&r:0,top)) < (r?((&r:1,top)) + -2)) } else { 0 } } }
} } else { <error> }
} } else { <error> } : if ((0 < r?((&r:0,top)))) { {
if ((0 < r?((&r:2,top)))) { {
Expand All @@ -66,7 +66,7 @@
} } else { r?((&r:1,top)) } : "int" ],"&leader_len" -> [ r?((&r:0,top)) : "int" ],"&p" -> [ if ((0 < r?((&r:0,top)))) { {
if ((0 < r?((&r:2,top)))) { {
if ((r?((&r:1,top)) < r?((&r:0,top)))) { <error> } else { {
if (((r?((&r:1,top)) + (r?((&r:0,top)) * -1)) < (r?((&r:2,top)) * 2))) { r?((&r:0,top)) } else { (r?((&r:0,top)) + (fixindex { x47? => if ((x47? < r?((&r:2,top)))) { (r?((&r:0,top)) < (r?((&r:1,top)) + -2)) } else { 0 } } * 2)) }
if (((r?((&r:1,top)) + (r?((&r:0,top)) * -1)) < (r?((&r:2,top)) * 2))) { r?((&r:0,top)) } else { (r?((&r:0,top)) + (fixindex { x59? => if ((x59? < r?((&r:2,top)))) { (r?((&r:0,top)) < (r?((&r:1,top)) + -2)) } else { 0 } } * 2)) }
} }
} } else { <error> }
} } else { <error> } : if ((0 < r?((&r:0,top)))) { {
Expand Down
2 changes: 1 addition & 1 deletion test-out/sv-bench/loop-invgen/fragtest_simple_true-unreach-call.i.check
View file
Expand Up @@ -42,4 +42,4 @@
return 0;
}
Final store:
{ "&j" -> [ if ((0 < fixindex { x85? => if (r?(("&r:2",("top",x85?)))) { (x85? < 1000001) } else { 0 } })) { (fixindex { x85? => if (r?(("&r:2",("top",x85?)))) { (x85? < 1000001) } else { 0 } } + -1) } else { 0 } : "int" ],"&i" -> [ if ((1 < fixindex { x85? => if (r?(("&r:2",("top",x85?)))) { (x85? < 1000001) } else { 0 } })) { 1 } else { fixindex { x85? => if (r?(("&r:2",("top",x85?)))) { (x85? < 1000001) } else { 0 } } } : "int" ],"valid" -> 1,"&n" -> [ fixindex { x85? => if (r?(("&r:2",("top",x85?)))) { (x85? < 1000001) } else { 0 } } : "int" ],"&tmp___1" -> [ if ((0 < fixindex { x85? => if (r?(("&r:2",("top",x85?)))) { (x85? < 1000001) } else { 0 } })) { (fixindex { x85? => if (r?(("&r:2",("top",x85?)))) { (x85? < 1000001) } else { 0 } } + -1) } else { <error> } : if ((0 < fixindex { x85? => if (r?(("&r:2",("top",x85?)))) { (x85? < 1000001) } else { 0 } })) { "int" } else { <error> } ],"&k" -> [ if ((1 < fixindex { x85? => if (r?(("&r:2",("top",x85?)))) { (x85? < 1000001) } else { 0 } })) { 1 } else { fixindex { x85? => if (r?(("&r:2",("top",x85?)))) { (x85? < 1000001) } else { 0 } } } : "int" ],"return" -> [ 0 : "int" ],"&pvlen" -> [ if ((r?((&r:0,top)) < fixindex { x8? => if (r?(("&r:1",("top",x8?)))) { (x8? < 1000001) } else { 0 } })) { fixindex { x8? => if (r?(("&r:1",("top",x8?)))) { (x8? < 1000001) } else { 0 } } } else { r?((&r:0,top)) } : "int" ] }
{ "&j" -> [ if ((0 < fixindex { x91? => if (r?(("&r:2",("top",x91?)))) { (x91? < 1000001) } else { 0 } })) { (fixindex { x91? => if (r?(("&r:2",("top",x91?)))) { (x91? < 1000001) } else { 0 } } + -1) } else { 0 } : "int" ],"&i" -> [ if ((1 < fixindex { x91? => if (r?(("&r:2",("top",x91?)))) { (x91? < 1000001) } else { 0 } })) { 1 } else { fixindex { x91? => if (r?(("&r:2",("top",x91?)))) { (x91? < 1000001) } else { 0 } } } : "int" ],"valid" -> 1,"&n" -> [ fixindex { x91? => if (r?(("&r:2",("top",x91?)))) { (x91? < 1000001) } else { 0 } } : "int" ],"&tmp___1" -> [ if ((0 < fixindex { x91? => if (r?(("&r:2",("top",x91?)))) { (x91? < 1000001) } else { 0 } })) { (fixindex { x91? => if (r?(("&r:2",("top",x91?)))) { (x91? < 1000001) } else { 0 } } + -1) } else { <error> } : if ((0 < fixindex { x91? => if (r?(("&r:2",("top",x91?)))) { (x91? < 1000001) } else { 0 } })) { "int" } else { <error> } ],"&k" -> [ if ((1 < fixindex { x91? => if (r?(("&r:2",("top",x91?)))) { (x91? < 1000001) } else { 0 } })) { 1 } else { fixindex { x91? => if (r?(("&r:2",("top",x91?)))) { (x91? < 1000001) } else { 0 } } } : "int" ],"return" -> [ 0 : "int" ],"&pvlen" -> [ if ((r?((&r:0,top)) < fixindex { x8? => if (r?(("&r:1",("top",x8?)))) { (x8? < 1000001) } else { 0 } })) { fixindex { x8? => if (r?(("&r:1",("top",x8?)))) { (x8? < 1000001) } else { 0 } } } else { r?((&r:0,top)) } : "int" ] }
4 changes: 3 additions & 1 deletion test-out/sv-bench/loop-invgen/large_const_true-unreach-call.i.check
View file
Expand Up @@ -39,4 +39,6 @@
return 0;
}
Final store:
{ "&j" -> [ if ((0 < r?((&r:0,top)))) { r?((&r:0,top)) } else { 0 } : "int" ],"&i" -> [ if ((0 < r?((&r:0,top)))) { r?((&r:0,top)) } else { 0 } : "int" ],"&c2" -> [ 2000 : "int" ],"&v" -> [ if ((0 < r?((&r:0,top)))) { r?(("&r:1",("top",(r?((&r:0,top)) + -1)))) } else { <error> } : if ((0 < r?((&r:0,top)))) { "int" } else { <error> } ],"valid" -> 1,"&n" -> [ r?((&r:0,top)) : "int" ],"&k" -> [ if ((0 < r?((&r:0,top)))) { (sum(r?((&r:0,top))) { x22?x21_&k_$value? => if ((r?(("&r:1",("top",x22?x21_&k_$value?))) == 0)) { 4000 } else { 2000 } } + (r?((&r:0,top)) * -1)) } else { 0 } : "int" ],"&c1" -> [ 4000 : "int" ],"return" -> [ 0 : "int" ],"&c3" -> [ 10000 : "int" ] }
{ "&j" -> [ r?((&r:0,top)) : "int" ],"&i" -> [ r?((&r:0,top)) : "int" ],"&c2" -> [ 2000 : "int" ],"&v" -> [ if ((0 < r?((&r:0,top)))) { {
if ((r?(("&r:1",("top",(r?((&r:0,top)) + -1)))) == 0)) { 0 } else { 1 }
} } else { <error> } : if ((0 < r?((&r:0,top)))) { "int" } else { <error> } ],"valid" -> 1,"&n" -> [ r?((&r:0,top)) : "int" ],"&k" -> [ (sum(r?((&r:0,top))) { x22?x21_&k_$value? => if ((r?(("&r:1",("top",x22?x21_&k_$value?))) == 0)) { 4000 } else { 2000 } } + (r?((&r:0,top)) * -1)) : "int" ],"&c1" -> [ 4000 : "int" ],"return" -> [ 0 : "int" ],"&c3" -> [ 10000 : "int" ] }
2 changes: 1 addition & 1 deletion test-out/sv-bench/loop-invgen/nested6_true-unreach-call.i.check
View file
Expand Up @@ -37,7 +37,7 @@
Final store:
{ "&j" -> [ if ((r?((&r:0,top)) == r?((&r:1,top)))) { {
if ((0 < r?((&r:1,top)))) { {
if ((r?((&r:1,top)) < 2)) { r?((&r:1,top)) } else { ((r?((&r:1,top)) * 2) + -2) }
if ((r?((&r:1,top)) < 2)) { 1 } else { ((r?((&r:1,top)) * 2) + -2) }
} } else { <error> }
} } else { <error> } : if ((r?((&r:0,top)) == r?((&r:1,top)))) { {
if ((0 < r?((&r:1,top)))) { "int" } else { <error> }
Expand Down
2 changes: 1 addition & 1 deletion test-out/sv-bench/loop-lit/bhmr2007_true-unreach-call.c.i.check
View file
Expand Up @@ -27,4 +27,4 @@
return 0;
}
Final store:
{ "&i" -> [ if ((0 < r?((&r:0,top)))) { r?((&r:0,top)) } else { 0 } : "int" ],"valid" -> 1,"&a" -> [ if ((0 < r?((&r:0,top)))) { sum(r?((&r:0,top))) { x17?x16_&a_$value? => if (r?(("&r:1",("top",x17?x16_&a_$value?)))) { 1 } else { 2 } } } else { 0 } : "int" ],"&n" -> [ r?((&r:0,top)) : "int" ],"&b" -> [ if ((0 < r?((&r:0,top)))) { sum(r?((&r:0,top))) { x17?x16_&b_$value? => if (r?(("&r:1",("top",x17?x16_&b_$value?)))) { 2 } else { 1 } } } else { 0 } : "int" ],"return" -> [ 0 : "int" ] }
{ "&i" -> [ r?((&r:0,top)) : "int" ],"valid" -> 1,"&a" -> [ sum(r?((&r:0,top))) { x17?x16_&a_$value? => if (r?(("&r:1",("top",x17?x16_&a_$value?)))) { 1 } else { 2 } } : "int" ],"&n" -> [ r?((&r:0,top)) : "int" ],"&b" -> [ sum(r?((&r:0,top))) { x17?x16_&b_$value? => if (r?(("&r:1",("top",x17?x16_&b_$value?)))) { 2 } else { 1 } } : "int" ],"return" -> [ 0 : "int" ] }
2 changes: 1 addition & 1 deletion test-out/sv-bench/loop-lit/ddlm2013_true-unreach-call.c.i.check
View file
Expand Up @@ -36,4 +36,4 @@
return 0;
}
Final store:
{ "&j" -> [ if (r?((&r:0,top))) { ((fixindex { x17? => r?(("&r:1",("top",x17?))) } * 2) + 1) } else { (fixindex { x17? => r?(("&r:1",("top",x17?))) } + 1) } : "int" ],"&i" -> [ if (r?((&r:0,top))) { (fixindex { x17? => r?(("&r:1",("top",x17?))) } * 2) } else { ((fixindex { x17? => r?(("&r:1",("top",x17?))) } * 2) + 1) } : "int" ],"valid" -> 1,"&a" -> [ fixindex { x17? => r?(("&r:1",("top",x17?))) } : "int" ],"&flag" -> [ r?((&r:0,top)) : "int" ],"&b" -> [ if (r?((&r:0,top))) { fixindex { x17? => r?(("&r:1",("top",x17?))) } } else { sum(fixindex { x17? => r?(("&r:1",("top",x17?))) }) { x17?x16_&b_$value? => (x17?x16_&b_$value? * -1) } } : "int" ],"return" -> [ 0 : "int" ] }
{ "&j" -> [ if (r?((&r:0,top))) { ((fixindex { x24? => r?(("&r:1",("top",x24?))) } * 2) + 1) } else { (fixindex { x24? => r?(("&r:1",("top",x24?))) } + 1) } : "int" ],"&i" -> [ if (r?((&r:0,top))) { (fixindex { x24? => r?(("&r:1",("top",x24?))) } * 2) } else { ((fixindex { x24? => r?(("&r:1",("top",x24?))) } * 2) + 1) } : "int" ],"valid" -> 1,"&a" -> [ fixindex { x24? => r?(("&r:1",("top",x24?))) } : "int" ],"&flag" -> [ if (r?((&r:0,top))) { 1 } else { 0 } : "int" ],"&b" -> [ if (r?((&r:0,top))) { fixindex { x24? => r?(("&r:1",("top",x24?))) } } else { sum(fixindex { x24? => r?(("&r:1",("top",x24?))) }) { x24?x23_&b_$value? => (x24?x23_&b_$value? * -1) } } : "int" ],"return" -> [ 0 : "int" ] }
2 changes: 1 addition & 1 deletion test-out/sv-bench/loop-lit/hhk2008_true-unreach-call.c.i.check
View file
Expand Up @@ -25,4 +25,4 @@
return 0;
}
Final store:
{ "&cnt" -> [ if ((0 < r?((&r:1,top)))) { 0 } else { r?((&r:1,top)) } : "int" ],"valid" -> 1,"&a" -> [ r?((&r:0,top)) : "int" ],"&b" -> [ r?((&r:1,top)) : "int" ],"return" -> [ 0 : "int" ],"&res" -> [ if ((0 < r?((&r:1,top)))) { (r?((&r:0,top)) + r?((&r:1,top))) } else { r?((&r:0,top)) } : "int" ] }
{ "&cnt" -> [ 0 : "int" ],"valid" -> 1,"&a" -> [ r?((&r:0,top)) : "int" ],"&b" -> [ r?((&r:1,top)) : "int" ],"return" -> [ 0 : "int" ],"&res" -> [ (r?((&r:0,top)) + r?((&r:1,top))) : "int" ] }
2 changes: 1 addition & 1 deletion test-out/sv-bench/loop-lit/jm2006_true-unreach-call.c.i.check
View file
Expand Up @@ -26,4 +26,4 @@
return 0;
}
Final store:
{ "&j" -> [ r?((&r:1,top)) : "int" ],"&i" -> [ r?((&r:0,top)) : "int" ],"valid" -> 1,"&x" -> [ if ((0 < r?((&r:0,top)))) { 0 } else { r?((&r:0,top)) } : "int" ],"&y" -> [ if ((0 < r?((&r:0,top)))) { (r?((&r:1,top)) + (r?((&r:0,top)) * -1)) } else { r?((&r:1,top)) } : "int" ],"return" -> [ 0 : "int" ] }
{ "&j" -> [ r?((&r:1,top)) : "int" ],"&i" -> [ r?((&r:0,top)) : "int" ],"valid" -> 1,"&x" -> [ 0 : "int" ],"&y" -> [ (r?((&r:1,top)) + (r?((&r:0,top)) * -1)) : "int" ],"return" -> [ 0 : "int" ] }
2 changes: 1 addition & 1 deletion test-out/sv-bench/loop-lit/jm2006_variant_true-unreach-call.c.i.check
View file
Expand Up @@ -29,4 +29,4 @@
return 0;
}
Final store:
{ "&j" -> [ r?((&r:1,top)) : "int" ],"&i" -> [ r?((&r:0,top)) : "int" ],"valid" -> 1,"&x" -> [ if ((0 < r?((&r:0,top)))) { 0 } else { r?((&r:0,top)) } : "int" ],"&z" -> [ if ((0 < r?((&r:0,top)))) { r?((&r:0,top)) } else { 0 } : "int" ],"&y" -> [ if ((0 < r?((&r:0,top)))) { (r?((&r:1,top)) + (r?((&r:0,top)) * -2)) } else { r?((&r:1,top)) } : "int" ],"return" -> [ 0 : "int" ] }
{ "&j" -> [ r?((&r:1,top)) : "int" ],"&i" -> [ r?((&r:0,top)) : "int" ],"valid" -> 1,"&x" -> [ 0 : "int" ],"&z" -> [ r?((&r:0,top)) : "int" ],"&y" -> [ (r?((&r:1,top)) + (r?((&r:0,top)) * -2)) : "int" ],"return" -> [ 0 : "int" ] }
4 changes: 2 additions & 2 deletions test-out/sv-bench/loop-lit/mcmillan2006_true-unreach-call.c.i.check
View file
Expand Up @@ -19,8 +19,8 @@
return 0;
}
Final store:
{ "&i" -> [ if ((0 < r?((&r:0,top)))) { r?((&r:0,top)) } else { 0 } : "int" ],"valid" -> 1,"&n" -> [ r?((&r:0,top)) : "int" ],"&x" -> [ (&new:0,top) : "int * *" ],"return" -> [ 0 : "int" ],"&new:0" -> { "top" -> [ if ((0 < r?((&r:0,top)))) { collect(r?((&r:0,top))) { x14? =>
{ "&i" -> [ r?((&r:0,top)) : "int" ],"valid" -> 1,"&n" -> [ r?((&r:0,top)) : "int" ],"&x" -> [ (&new:0,top) : "int * *" ],"return" -> [ 0 : "int" ],"&new:0" -> { "top" -> [ if ((0 < r?((&r:0,top)))) { collect(r?((&r:0,top))) { x14? =>
0
} } else { collect(r?((&r:0,top))) { x14? =>
} } else { collect(0) { x14? =>
<error>
} } : "int *" ] } }

0 comments on commit 36146b9

Please sign in to comment.