From da24f881723ded2872eccdff740d66446b81d3ce Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Thu, 5 Aug 2021 20:39:50 +0200 Subject: [PATCH 01/17] Fixed simplifyGenericArrayRead --- .../java/hu/bme/mit/theta/core/utils/ExprSimplifier.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index dbe0a8d5b1..401fe43090 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java @@ -412,7 +412,12 @@ private static Expr simplifyArrayRead(final ArrayReadExpr expr, final V Expr> arr = simplify(expr.getArray(), val); Expr index = simplify(expr.getIndex(), val); if (arr instanceof LitExpr && index instanceof LitExpr) { - return expr.eval(val); + ArrayLitExpr arrayLit = (ArrayLitExpr) arr.eval(val); + for (Tuple2, Expr> element : arrayLit.getElements()) { + if (element.get1().equals(index)){ + return simplify(element.get2(), val); + } + } } return expr.with(arr, index); } From 2b4903bae02dbdb2aa83ffb52fc487e255959aca Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Thu, 5 Aug 2021 20:47:51 +0200 Subject: [PATCH 02/17] Added missing imports --- .../main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index 401fe43090..4dd6d9452f 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java @@ -16,6 +16,7 @@ package hu.bme.mit.theta.core.utils; import hu.bme.mit.theta.common.DispatchTable2; +import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; @@ -23,6 +24,7 @@ import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.anytype.IteExpr; import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr; From 129683b96c68b5d2c7ea00207cb5dbe3ff1c5471 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 5 Aug 2021 20:57:14 +0200 Subject: [PATCH 03/17] Added else branch for arrayreadexpr simplification --- .../main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java | 1 + 1 file changed, 1 insertion(+) diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index 4dd6d9452f..c46919f3ed 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java @@ -420,6 +420,7 @@ private static Expr simplifyArrayRead(final ArrayReadExpr expr, final V return simplify(element.get2(), val); } } + return simplify(arrayLit.getElseElem(), val); } return expr.with(arr, index); } From 34889eb215596e4b895d99797ff571cc62b3f8e5 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 5 Aug 2021 21:14:15 +0200 Subject: [PATCH 04/17] ArrayLitExpr shall only take literals --- .../bme/mit/theta/cfa/dsl/CfaExpression.java | 2 +- .../theta/core/type/arraytype/ArrayExprs.java | 2 +- .../core/type/arraytype/ArrayLitExpr.java | 35 +++++--- .../core/type/arraytype/ArrayReadExpr.java | 17 ++-- .../core/type/arraytype/ArrayWriteExpr.java | 21 +++-- .../mit/theta/core/utils/ExprSimplifier.java | 10 +-- .../mit/theta/core/expr/EvaluationTest.java | 33 ++++---- .../theta/core/utils/ExprCanonizerTest.java | 4 +- .../theta/core/utils/ExprSimplifierTest.java | 4 +- .../mit/theta/xsts/dsl/XstsExpression.java | 79 +++++++++++++++++-- 10 files changed, 136 insertions(+), 71 deletions(-) diff --git a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java index d1c944aac8..6275664a77 100644 --- a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java +++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java @@ -1030,7 +1030,7 @@ private Expr createArrayLitExpr(final ArrL } valueType = (T2) ctx.elseExpr.accept(this).getType(); - final List, Expr>> elems = IntStream + final List, ? extends Expr>> elems = IntStream .range(0, ctx.indexExpr.size()) .mapToObj(i -> Tuple2.of( cast(ctx.indexExpr.get(i).accept(this), indexType), diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayExprs.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayExprs.java index 421d87b586..9010ee1f1b 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayExprs.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayExprs.java @@ -32,7 +32,7 @@ public static ArrayType ArrayLitExpr Array( - final List, Expr>> elems, final Expr elseElem, + final List, ? extends Expr>> elems, final Expr elseElem, final ArrayType type) { return ArrayLitExpr.of(elems, elseElem, type); } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayLitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayLitExpr.java index 6dfae4aa2f..7cfb22f0c7 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayLitExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayLitExpr.java @@ -1,17 +1,21 @@ package hu.bme.mit.theta.core.type.arraytype; -import static com.google.common.base.Preconditions.checkNotNull; -import java.util.List; - import com.google.common.collect.ImmutableList; - import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.model.ImmutableValuation; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.core.type.NullaryExpr; import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.utils.ExprSimplifier; + +import java.util.List; +import java.util.stream.Collectors; + +import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; public final class ArrayLitExpr extends NullaryExpr> implements LitExpr> { @@ -21,27 +25,34 @@ public final class ArrayLitExpr e private final ArrayType type; - private final List, Expr>> elems; + private final List, LitExpr>> elems; - private final Expr elseElem; + private final LitExpr elseElem; private volatile int hashCode; - private ArrayLitExpr(final List, Expr>> elems, + private ArrayLitExpr(final List, ? extends Expr>> elems, final Expr elseElem, final ArrayType type) { this.type = checkNotNull(type); - this.elseElem = checkNotNull(elseElem); - this.elems = checkNotNull(elems); + Expr simplifiedElem = ExprSimplifier.simplify(checkNotNull(elseElem), ImmutableValuation.empty()); + checkState(simplifiedElem instanceof LitExpr, "ArrayLitExprs shall only contain literal values!"); + this.elseElem = (LitExpr) simplifiedElem; + this.elems = checkNotNull(elems).stream().map(elem -> { + Expr index = ExprSimplifier.simplify(elem.get1(), ImmutableValuation.empty()); + Expr element = ExprSimplifier.simplify(elem.get2(), ImmutableValuation.empty()); + checkState(index instanceof LitExpr && element instanceof LitExpr, "ArrayLitExprs shall only contain literal values"); + return Tuple2.of((LitExpr)index, (LitExpr)element); + }).collect(Collectors.toList()); } public static ArrayLitExpr of( - final List, Expr>> elems, + final List, ? extends Expr>> elems, final Expr elseElem, final ArrayType type) { return new ArrayLitExpr<>(elems, elseElem, type); } - public List, Expr>> getElements() { return ImmutableList.copyOf(elems); } + public List, LitExpr>> getElements() { return ImmutableList.copyOf(elems); } public Expr getElseElem() { return elseElem; } @@ -61,7 +72,7 @@ public int hashCode() { if (tmp == 0) { tmp = HASH_SEED; tmp = 31 * tmp + type.hashCode(); - for(Tuple2, Expr> elem : elems) { + for(Tuple2, LitExpr> elem : elems) { tmp = 31 * tmp + elem.hashCode(); } hashCode = tmp; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayReadExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayReadExpr.java index 6bee081a1d..98a29e1e1e 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayReadExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayReadExpr.java @@ -15,14 +15,7 @@ */ package hu.bme.mit.theta.core.type.arraytype; -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkNotNull; -import static hu.bme.mit.theta.core.utils.TypeUtils.cast; - -import java.util.List; - import com.google.common.collect.ImmutableList; - import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.model.Valuation; @@ -30,6 +23,12 @@ import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.core.type.Type; +import java.util.List; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; +import static hu.bme.mit.theta.core.utils.TypeUtils.cast; + public final class ArrayReadExpr implements Expr { private static final int HASH_SEED = 1321; @@ -76,9 +75,9 @@ public ElemType getType() { public LitExpr eval(final Valuation val) { ArrayLitExpr arrayVal = (ArrayLitExpr)array.eval(val); LitExpr indexVal = index.eval(val); - for (Tuple2, Expr> elem : arrayVal.getElements()) { + for (Tuple2, LitExpr> elem : arrayVal.getElements()) { if (elem.get1().equals(indexVal)){ - return (LitExpr)elem.get2(); + return elem.get2(); } } return (LitExpr)arrayVal.getElseElem(); diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayWriteExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayWriteExpr.java index 837a5aaad3..ae37955d79 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayWriteExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayWriteExpr.java @@ -15,16 +15,7 @@ */ package hu.bme.mit.theta.core.type.arraytype; -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkNotNull; -import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; -import static hu.bme.mit.theta.core.utils.TypeUtils.cast; - -import java.util.ArrayList; -import java.util.List; - import com.google.common.collect.ImmutableList; - import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.model.Valuation; @@ -32,6 +23,14 @@ import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.core.type.Type; +import java.util.ArrayList; +import java.util.List; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; +import static hu.bme.mit.theta.core.utils.TypeUtils.cast; + public final class ArrayWriteExpr implements Expr> { @@ -89,8 +88,8 @@ public LitExpr> eval(final Valuation val) { LitExpr indexVal = index.eval(val); LitExpr elemVal = elem.eval(val); - List, Expr>> elemList = new ArrayList<>(); - for(Tuple2, Expr> elem : arrayVal.getElements()) { + List, ? extends Expr>> elemList = new ArrayList<>(); + for(Tuple2, LitExpr> elem : arrayVal.getElements()) { if(!elem.get1().equals(indexVal)) { elemList.add(elem); } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index c46919f3ed..dbe0a8d5b1 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java @@ -16,7 +16,6 @@ package hu.bme.mit.theta.core.utils; import hu.bme.mit.theta.common.DispatchTable2; -import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; @@ -24,7 +23,6 @@ import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.anytype.IteExpr; import hu.bme.mit.theta.core.type.anytype.RefExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr; @@ -414,13 +412,7 @@ private static Expr simplifyArrayRead(final ArrayReadExpr expr, final V Expr> arr = simplify(expr.getArray(), val); Expr index = simplify(expr.getIndex(), val); if (arr instanceof LitExpr && index instanceof LitExpr) { - ArrayLitExpr arrayLit = (ArrayLitExpr) arr.eval(val); - for (Tuple2, Expr> element : arrayLit.getElements()) { - if (element.get1().equals(index)){ - return simplify(element.get2(), val); - } - } - return simplify(arrayLit.getElseElem(), val); + return expr.eval(val); } return expr.with(arr, index); } diff --git a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java index 091e6ee8c8..0b737c0768 100644 --- a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java +++ b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java @@ -15,9 +15,23 @@ */ package hu.bme.mit.theta.core.expr; +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.model.ImmutableValuation; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.inttype.IntType; +import org.junit.Test; + +import java.util.ArrayList; + import static hu.bme.mit.theta.core.decl.Decls.Const; import static hu.bme.mit.theta.core.type.anytype.Exprs.Ite; -import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.*; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Iff; @@ -56,19 +70,6 @@ import static hu.bme.mit.theta.core.type.rattype.RatExprs.ToInt; import static org.junit.Assert.assertEquals; -import hu.bme.mit.theta.common.Tuple2; -import org.junit.Test; - -import hu.bme.mit.theta.core.decl.ConstDecl; -import hu.bme.mit.theta.core.model.ImmutableValuation; -import hu.bme.mit.theta.core.model.Valuation; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.LitExpr; -import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.core.type.inttype.IntType; - -import java.util.ArrayList; - public class EvaluationTest { private final ConstDecl ca = Const("a", Int()); @@ -352,7 +353,7 @@ public void testRatSub() { @Test public void testRead() { - var elems = new ArrayList,Expr>>(); + var elems = new ArrayList, ? extends Expr>>(); elems.add(Tuple2.of(Int(0), Int(1))); elems.add(Tuple2.of(Int(1), Int(2))); var arr = Array(elems, Int(100), Array(Int(), Int())); @@ -363,7 +364,7 @@ public void testRead() { @Test public void testWrite() { - var elems = new ArrayList,Expr>>(); + var elems = new ArrayList, ? extends Expr>>(); elems.add(Tuple2.of(Int(0), Int(1))); elems.add(Tuple2.of(Int(1), Int(2))); var arr = Array(elems, Int(100), Array(Int(), Int())); diff --git a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprCanonizerTest.java b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprCanonizerTest.java index 8f925e03fd..b8c8832acb 100644 --- a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprCanonizerTest.java +++ b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprCanonizerTest.java @@ -488,7 +488,7 @@ public void testIte() { // Array @Test public void testArrayRead() { - var elems = new ArrayList,Expr>>(); + var elems = new ArrayList, ? extends Expr>>(); elems.add(Tuple2.of(Int(0), Int(1))); elems.add(Tuple2.of(Int(1), Int(2))); var arr = Array(elems, Int(100), Array(Int(), Int())); @@ -498,7 +498,7 @@ public void testArrayRead() { @Test public void testArrayWrite() { - var elems = new ArrayList,Expr>>(); + var elems = new ArrayList,? extends Expr>>(); elems.add(Tuple2.of(Int(0), Int(1))); var arr = Array(elems, Int(100), Array(Int(), Int())); assertEquals(Write(arr, Int(5), Int(6)), canonize(Write(arr, Int(5), Int(6)))); diff --git a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java index 335314f7c8..ef2bb34505 100644 --- a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java +++ b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java @@ -723,7 +723,7 @@ public void testIte() { // Array @Test public void testArrayRead() { - var elems = new ArrayList,Expr>>(); + var elems = new ArrayList, ? extends Expr>>(); elems.add(Tuple2.of(Int(0), Int(1))); elems.add(Tuple2.of(Int(1), Int(2))); var arr = Array(elems, Int(100), Array(Int(), Int())); @@ -734,7 +734,7 @@ public void testArrayRead() { @Test public void testArrayWrite() { - var elems = new ArrayList,Expr>>(); + var elems = new ArrayList, ? extends Expr>>(); elems.add(Tuple2.of(Int(0), Int(1))); var arr = Array(elems, Int(100), Array(Int(), Int())); var newArr = simplify(Write(arr, Int(5), Int(6))); diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java index 52ea25a7c3..13ef932020 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java @@ -2,19 +2,26 @@ import com.google.common.collect.ImmutableList; import hu.bme.mit.theta.common.Tuple2; -import hu.bme.mit.theta.common.dsl.*; +import hu.bme.mit.theta.common.dsl.DynamicScope; +import hu.bme.mit.theta.common.dsl.Env; +import hu.bme.mit.theta.common.dsl.Symbol; +import hu.bme.mit.theta.common.dsl.SymbolTable; import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.dsl.ParseException; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.core.type.abstracttype.*; +import hu.bme.mit.theta.core.type.abstracttype.AddExpr; +import hu.bme.mit.theta.core.type.abstracttype.DivExpr; +import hu.bme.mit.theta.core.type.abstracttype.ModExpr; +import hu.bme.mit.theta.core.type.abstracttype.MulExpr; +import hu.bme.mit.theta.core.type.abstracttype.RemExpr; +import hu.bme.mit.theta.core.type.abstracttype.SubExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.booltype.FalseExpr; import hu.bme.mit.theta.core.type.booltype.TrueExpr; import hu.bme.mit.theta.core.type.inttype.IntLitExpr; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslBaseVisitor; -import hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.*; import org.antlr.v4.runtime.Token; import java.math.BigInteger; @@ -29,14 +36,70 @@ import static com.google.common.base.Preconditions.checkNotNull; import static hu.bme.mit.theta.common.Utils.head; import static hu.bme.mit.theta.common.Utils.tail; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Add; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Div; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Geq; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Gt; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Ite; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Leq; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Lt; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Mod; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Mul; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Neg; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Neq; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*; -import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.*; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Pos; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Rem; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Sub; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Iff; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Or; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Xor; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.*; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.AccessContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.AccessorExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.AdditiveExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.AndExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ArrLitExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ArrayReadAccessContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ArrayWriteAccessContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.DIV; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.EQ; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.EqualityExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.FalseExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.GEQ; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.GT; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.IdExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.IffExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ImplyExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.IntLitExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.IteExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.LEQ; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.LT; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.MINUS; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.MOD; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.MUL; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.MultiplicativeExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.NEQ; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.NotExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.OrExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.PLUS; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ParenExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.REM; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.RelationExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.TrueExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.UnaryExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.XorExprContext; import static java.util.stream.Collectors.toList; final class XstsExpression { @@ -443,7 +506,7 @@ private Expr createArrayLitExpr(final ArrL } valueType = (T2) ctx.elseExpr.accept(this).getType(); - final List, Expr>> elems = IntStream + final List, ? extends Expr>> elems = IntStream .range(0, ctx.indexExpr.size()) .mapToObj(i -> Tuple2.of( cast(ctx.indexExpr.get(i).accept(this), indexType), From 7b3401f298a6038c7ee169190b2244281865f131 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 5 Aug 2021 21:50:38 +0200 Subject: [PATCH 05/17] Added ArrayInitExpr --- .../mit/theta/core/dsl/impl/ExprWriter.java | 10 ++ .../theta/core/type/arraytype/ArrayExprs.java | 10 +- .../core/type/arraytype/ArrayInitExpr.java | 92 +++++++++++++++++++ .../core/type/arraytype/package-info.java | 1 + .../mit/theta/core/utils/ExprSimplifier.java | 20 ++++ .../theta/core/utils/ExprSimplifierTest.java | 22 +++++ .../theta/solver/z3/Z3ExprTransformer.java | 11 +++ 7 files changed, 164 insertions(+), 2 deletions(-) create mode 100644 subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprWriter.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprWriter.java index d394a5e5e2..e09342f22f 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprWriter.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprWriter.java @@ -24,6 +24,7 @@ import hu.bme.mit.theta.core.type.anytype.PrimeExpr; import hu.bme.mit.theta.core.type.anytype.RefExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayEqExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayNeqExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; @@ -307,6 +308,8 @@ private ExprWriter() { .addCase(ArrayLitExpr.class, this::arrayLit) + .addCase(ArrayInitExpr.class, this::arrayInit) + // FloatingPoint .addCase(FpAbsExpr.class, e -> prefixUnary(e, " fpabs ")) @@ -470,5 +473,12 @@ private String arrayLit(final ArrayLitExpr expr) { "]"; } + private String arrayInit(final ArrayInitExpr expr) { + return "[" + + expr.getElements().stream().map(e -> write(e.get1()) + " <- " + write(e.get2())).collect(Collectors.joining(", ")) + + "<" + expr.getType().getIndexType().toString() + ">default" + " <- " + write(expr.getElseElem()) + + "]"; + } + } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayExprs.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayExprs.java index 9010ee1f1b..45b1e8afa1 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayExprs.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayExprs.java @@ -15,12 +15,12 @@ */ package hu.bme.mit.theta.core.type.arraytype; -import java.util.List; - import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; +import java.util.List; + public final class ArrayExprs { private ArrayExprs() { @@ -37,6 +37,12 @@ public static ArrayLitExpr ArrayInitExpr ArrayInit( + final List, Expr>> elems, final Expr elseElem, + final ArrayType type) { + return ArrayInitExpr.of(elems, elseElem, type); + } + public static ArrayReadExpr Read( final Expr> array, final Expr index) { return ArrayReadExpr.of(array, index); diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java new file mode 100644 index 0000000000..caeb8e8a58 --- /dev/null +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java @@ -0,0 +1,92 @@ +package hu.bme.mit.theta.core.type.arraytype; + +import com.google.common.collect.ImmutableList; +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.NullaryExpr; +import hu.bme.mit.theta.core.type.Type; + +import java.util.List; +import java.util.stream.Collectors; + +import static com.google.common.base.Preconditions.checkNotNull; + +public final class ArrayInitExpr extends NullaryExpr> { + + private static final int HASH_SEED = 229; + private static final String OPERATOR_LABEL = "arrayinit"; + + private final ArrayType type; + + private final List, Expr>> elems; + + private final Expr elseElem; + + private volatile int hashCode; + + private ArrayInitExpr(final List, Expr>> elems, + final Expr elseElem, final ArrayType type) { + this.type = checkNotNull(type); + this.elseElem = checkNotNull(elseElem); + this.elems = checkNotNull(elems); + } + + public static ArrayInitExpr of( + final List, Expr>> elems, + final Expr elseElem, + final ArrayType type) { + return new ArrayInitExpr<>(elems, elseElem, type); + } + + public List, Expr>> getElements() { return ImmutableList.copyOf(elems); } + + public Expr getElseElem() { return elseElem; } + + @Override + public ArrayType getType() { + return type; + } + + @Override + public LitExpr> eval(final Valuation val) { + return ArrayLitExpr.of(elems.stream().map(objects -> Tuple2.of(objects.get1().eval(val), objects.get2().eval(val))).collect(Collectors.toList()), elseElem, type); + } + + @Override + public int hashCode() { + int tmp = hashCode; + if (tmp == 0) { + tmp = HASH_SEED; + tmp = 31 * tmp + type.hashCode(); + for(Tuple2, Expr> elem : elems) { + tmp = 31 * tmp + elem.hashCode(); + } + hashCode = tmp; + } + return tmp; + } + + @Override + public boolean equals(final Object obj) { + if (this == obj) { + return true; + } else if (obj instanceof ArrayInitExpr) { + final ArrayInitExpr that = (ArrayInitExpr) obj; + return this.type.equals(that.type) && this.elems.equals(that.elems); + } else { + return false; + } + } + + @Override + public String toString() { + return Utils.lispStringBuilder(OPERATOR_LABEL) + .addAll(elems.stream().map(elem -> String.format("(%s %s)", elem.get1(), elem.get2()))) + .add((String.format("(default %s)", elseElem))) + .toString(); + } + +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/package-info.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/package-info.java index 2f43083159..acd2166f5a 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/package-info.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/package-info.java @@ -5,6 +5,7 @@ * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayType}: the actual array type * * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr}: array literal, e.g., [0 <- 182, 1 <- 41, default <- 75] + * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr}: array init expression, e.g., [0 <- 182, 1 <- x, default <- 75] * * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr}: read array at an index, e.g., a[i] * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr}: write array at an index, e.g., a[i <- v], diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index dbe0a8d5b1..14f1fb59b6 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java @@ -16,6 +16,7 @@ package hu.bme.mit.theta.core.utils; import hu.bme.mit.theta.common.DispatchTable2; +import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; @@ -23,6 +24,7 @@ import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.anytype.IteExpr; import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr; @@ -223,6 +225,8 @@ public final class ExprSimplifier { .addCase(ArrayWriteExpr.class, ExprSimplifier::simplifyArrayWrite) + .addCase(ArrayInitExpr.class, ExprSimplifier::simplifyArrayInit) + // Bitvectors .addCase(BvConcatExpr.class, ExprSimplifier::simplifyBvConcat) @@ -432,6 +436,22 @@ private static Expr simplifyArrayWrite(final ArrayWriteExpr expr, final return expr.with(arr, index, elem); } + private static Expr> + simplifyArrayInit(final ArrayInitExpr t, final Valuation val) { + boolean nonLiteralFound = false; + List, Expr>> newElements = new ArrayList<>(); + Expr newElseElem = simplify(t.getElseElem(), val); + if(!(newElseElem instanceof LitExpr)) nonLiteralFound = true; + for (Tuple2, Expr> element : t.getElements()) { + Expr newIndex = simplify(element.get1(), val); + Expr newElement = simplify(element.get2(), val); + newElements.add(Tuple2.of(newIndex, newElement)); + if(!(newElement instanceof LitExpr) || !(newIndex instanceof LitExpr)) nonLiteralFound = true; + } + if(nonLiteralFound) return ArrayInitExpr.of(newElements, newElseElem, t.getType()); + else return t.eval(val); + } + /* * Booleans */ diff --git a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java index ef2bb34505..2b2de34a11 100644 --- a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java +++ b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java @@ -17,10 +17,14 @@ import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.model.ImmutableValuation; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.bvtype.BvExprs; import hu.bme.mit.theta.core.type.bvtype.BvType; @@ -32,8 +36,10 @@ import java.util.List; import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.decl.Decls.Var; import static hu.bme.mit.theta.core.type.anytype.Exprs.Ite; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.ArrayInit; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; @@ -76,6 +82,7 @@ import static hu.bme.mit.theta.core.type.rattype.RatExprs.ToInt; import static hu.bme.mit.theta.core.utils.ExprUtils.simplify; import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertFalse; import static org.junit.Assert.assertTrue; public class ExprSimplifierTest { @@ -744,6 +751,21 @@ public void testArrayWrite() { assertEquals(Int(100), Read(newArr, Int(182)).eval(ImmutableValuation.empty())); } + @Test + public void testArrayInit() { + var elems = new ArrayList, Expr>>(); + elems.add(Tuple2.of(Int(0), Int(1))); + elems.add(Tuple2.of(Int(1), Add(Int(1), Int(2)))); + VarDecl noname = Var("noname", Int()); + elems.add(Tuple2.of(Int(2), Add(noname.getRef(), Int(1)))); + var arr = ArrayInit(elems, Int(100), Array(Int(), Int())); + var newArr = simplify(arr); + assertTrue(newArr instanceof ArrayInitExpr); + assertEquals(Int(1), Read(newArr, Int(2)).eval(ImmutableValuation.builder().put(noname, Int(0)).build())); + assertFalse(simplify(Read(newArr, Int(2))) instanceof LitExpr); + assertTrue(simplify(Read(newArr, Int(2))) instanceof ArrayReadExpr); + } + @Test public void testComplex() { assertEquals(True(), simplify(Iff(And(x, True()), Or(x, False())))); diff --git a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java index e31976fb62..98dfcbb4db 100644 --- a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java +++ b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java @@ -35,6 +35,7 @@ import hu.bme.mit.theta.core.type.anytype.IteExpr; import hu.bme.mit.theta.core.type.anytype.RefExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayEqExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayNeqExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; @@ -391,6 +392,8 @@ public Z3ExprTransformer(final Z3TransformationManager transformer, final Contex .addCase(ArrayLitExpr.class, this::transformArrayLit) + .addCase(ArrayInitExpr.class, this::transformArrayInit) + .build(); } @@ -1149,6 +1152,14 @@ private com.microsoft.z3.Expr transformArrayLit(final ArrayLitExpr expr) { return running; } + private com.microsoft.z3.Expr transformArrayInit(final ArrayInitExpr expr) { + com.microsoft.z3.ArrayExpr running = context.mkConstArray(transformer.toSort(expr.getType().getIndexType()), toTerm(expr.getElseElem())); + for (Tuple2, ? extends Expr> elem : expr.getElements()) { + running = context.mkStore(running, toTerm(elem.get1()), toTerm(elem.get2())); + } + return running; + } + private com.microsoft.z3.Expr transformFuncApp(final FuncAppExpr expr) { final Tuple2, List>> funcAndArgs = extractFuncAndArgs(expr); final Expr func = funcAndArgs.get1(); From c5fd6e9b9e04831ae0e0cc339b199e6b15290bdb Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 5 Aug 2021 22:04:32 +0200 Subject: [PATCH 06/17] Added tests for ArrayInitExpr --- .../mit/theta/core/expr/EvaluationTest.java | 21 ++++++++ .../bme/mit/theta/solver/z3/Z3SolverTest.java | 48 ++++++++++++++++--- 2 files changed, 62 insertions(+), 7 deletions(-) diff --git a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java index 0b737c0768..97e386294f 100644 --- a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java +++ b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java @@ -17,6 +17,7 @@ import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.model.ImmutableValuation; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; @@ -28,8 +29,10 @@ import java.util.ArrayList; import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.decl.Decls.Var; import static hu.bme.mit.theta.core.type.anytype.Exprs.Ite; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.ArrayInit; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; @@ -381,6 +384,24 @@ public void testWrite() { assertEquals(Int(100), evaluate(Read(arr2, Int(5)))); } + @Test + public void testArrayInit() { + var elems = new ArrayList, Expr>>(); + VarDecl noname = Var("noname", Int()); + elems.add(Tuple2.of(Int(0), Int(1))); + elems.add(Tuple2.of(Int(1), Int(2))); + elems.add(Tuple2.of(Int(2), Add(noname.getRef(), Int(3)))); + var arr = ArrayInit(elems, Int(100), Array(Int(), Int())); + + ImmutableValuation val = ImmutableValuation.builder().put(noname, Int(1)).build(); + assertEquals(Int(1), evaluate(Read(arr, Int(0)), val)); + assertEquals(Int(2), evaluate(Read(arr, Int(1)), val)); + assertEquals(Int(4), evaluate(Read(arr, Int(2)), val)); + assertEquals(Int(100), evaluate(Read(arr, Int(5)), val)); + } + + + // anytype @Test diff --git a/subprojects/common/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java b/subprojects/common/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java index fea7d0b611..e9a2517f35 100644 --- a/subprojects/common/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java +++ b/subprojects/common/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java @@ -15,19 +15,13 @@ */ package hu.bme.mit.theta.solver.z3; +import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.decl.ParamDecl; import hu.bme.mit.theta.core.model.ImmutableValuation; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.LitExpr; - -import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; -import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read; -import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; -import static hu.bme.mit.theta.core.type.bvtype.BvExprs.Bv; - import hu.bme.mit.theta.core.type.arraytype.ArrayExprs; import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayType; @@ -47,15 +41,24 @@ import org.junit.Test; import java.math.BigInteger; +import java.util.ArrayList; import java.util.List; import java.util.Optional; import static com.google.common.collect.ImmutableList.of; import static hu.bme.mit.theta.core.decl.Decls.Const; import static hu.bme.mit.theta.core.decl.Decls.Param; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.ArrayInit; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static hu.bme.mit.theta.core.type.bvtype.BvExprs.Bv; import static hu.bme.mit.theta.core.type.bvtype.BvExprs.BvType; import static hu.bme.mit.theta.core.type.functype.FuncExprs.App; import static hu.bme.mit.theta.core.type.functype.FuncExprs.Func; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Add; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static org.junit.Assert.assertEquals; import static org.junit.Assert.assertNotNull; @@ -152,6 +155,37 @@ public void testArray() { assertEquals(Int(2), Read(valLit, Int(1)).eval(ImmutableValuation.empty())); } + @Test + public void testArrayInit() { + final ConstDecl> arr = Const("arr", Array(Int(), Int())); + var elems = new ArrayList, Expr>>(); + ConstDecl noname = Const("noname", Int()); + elems.add(Tuple2.of(Int(0), Int(1))); + elems.add(Tuple2.of(Int(1), Int(2))); + elems.add(Tuple2.of(Int(2), Add(noname.getRef(), Int(3)))); + var initarr = ArrayInit(elems, Int(100), Array(Int(), Int())); + + solver.add(ArrayExprs.Eq(arr.getRef(), initarr)); + + // Check, the expression should be satisfiable + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + solver.add(Eq(noname.getRef(), Int(1))); + status = solver.check(); + assertTrue(status.isSat()); + + Valuation valuation = solver.getModel(); + final Optional>> optVal = valuation.eval(arr); + assertTrue(optVal.isPresent()); + final Expr> val = optVal.get(); + assertTrue(val instanceof ArrayLitExpr); + var valLit = (ArrayLitExpr)val; + assertEquals(Int(1), Read(valLit, Int(0)).eval(ImmutableValuation.empty())); + assertEquals(Int(2), Read(valLit, Int(1)).eval(ImmutableValuation.empty())); + assertEquals(Int(4), Read(valLit, Int(2)).eval(ImmutableValuation.empty())); + } + @Test public void testReset() { final ConstDecl cx = Const("x", Int()); From 94996339c1603aed052b007c9559e427d22cacb2 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 5 Aug 2021 22:09:05 +0200 Subject: [PATCH 07/17] Modified HASH_SEED of ArrayInitExpr to not match ArrayLitExpr --- .../hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java index caeb8e8a58..d197093db2 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java @@ -16,7 +16,7 @@ public final class ArrayInitExpr extends NullaryExpr> { - private static final int HASH_SEED = 229; + private static final int HASH_SEED = 241; private static final String OPERATOR_LABEL = "arrayinit"; private final ArrayType type; From f91d799b2aceeaa5f91042908dd2047ded864b72 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 5 Aug 2021 22:26:23 +0200 Subject: [PATCH 08/17] Fixed equals() method for both Array{Init,Lit}Expr --- .../hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java | 2 +- .../java/hu/bme/mit/theta/core/type/arraytype/ArrayLitExpr.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java index d197093db2..b45ebf9087 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java @@ -75,7 +75,7 @@ public boolean equals(final Object obj) { return true; } else if (obj instanceof ArrayInitExpr) { final ArrayInitExpr that = (ArrayInitExpr) obj; - return this.type.equals(that.type) && this.elems.equals(that.elems); + return this.type.equals(that.type) && this.elems.equals(that.elems) && elseElem.equals(that.elseElem); } else { return false; } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayLitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayLitExpr.java index 7cfb22f0c7..999a839753 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayLitExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayLitExpr.java @@ -86,7 +86,7 @@ public boolean equals(final Object obj) { return true; } else if (obj instanceof ArrayLitExpr) { final ArrayLitExpr that = (ArrayLitExpr) obj; - return this.type.equals(that.type) && this.elems.equals(that.elems); + return this.type.equals(that.type) && this.elems.equals(that.elems) && elseElem.equals(that.elseElem); } else { return false; } From d518ce6a6bc9601e1efe6d6b485778d6d296cd7a Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 5 Aug 2021 23:09:48 +0200 Subject: [PATCH 09/17] Added ArrayInit test CFA, modified ArrayInitExpr to be Multiary --- .../bme/mit/theta/cfa/analysis/CfaTest.java | 2 + .../src/test/resources/arrayinit.cfa | 20 +++++++ subprojects/cfa/cfa/README.md | 2 +- .../bme/mit/theta/cfa/dsl/CfaExpression.java | 7 ++- .../core/type/arraytype/ArrayInitExpr.java | 58 ++++++++++++------- 5 files changed, 64 insertions(+), 25 deletions(-) create mode 100644 subprojects/cfa/cfa-analysis/src/test/resources/arrayinit.cfa diff --git a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java index 159a1e5007..b6374b90a5 100644 --- a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java +++ b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java @@ -98,6 +98,8 @@ public static Collection data() { { "src/test/resources/arrays.cfa", PRED_BOOL, BW_BIN_ITP, false, 8 }, + { "src/test/resources/arrayinit.cfa", PRED_CART, BW_BIN_ITP, false, 4 }, + { "src/test/resources/arrays.cfa", EXPL, SEQ_ITP, false, 8 }, { "src/test/resources/counter5_true.cfa", PRED_BOOL, SEQ_ITP, true, 0 }, diff --git a/subprojects/cfa/cfa-analysis/src/test/resources/arrayinit.cfa b/subprojects/cfa/cfa-analysis/src/test/resources/arrayinit.cfa new file mode 100644 index 0000000000..6a3f753246 --- /dev/null +++ b/subprojects/cfa/cfa-analysis/src/test/resources/arrayinit.cfa @@ -0,0 +1,20 @@ +main process cfa { + var arr: [int]->int + var asd: int + + init loc L0 + loc L01 + loc L1 + loc L2 + final loc END + error loc ERR + + L0 -> L01 { asd := 1} + L01 -> L1 { arr := [ 0 <- 1, 1 <- asd + 2, default <- 0 ] } + + L1 -> L2 { assume arr[0] = 1 and arr[34] = 0 } + L1 -> ERR { assume not (arr[0] = 1 and arr[34] = 0) } + + L2 -> END { assume arr[1] = 2 } + L2 -> ERR { assume not (arr[1] = 2) } +} \ No newline at end of file diff --git a/subprojects/cfa/cfa/README.md b/subprojects/cfa/cfa/README.md index f8046e8f3f..1457a7f9c4 100644 --- a/subprojects/cfa/cfa/README.md +++ b/subprojects/cfa/cfa/README.md @@ -44,7 +44,7 @@ Variables of the CFA can have the following types. Expressions of the CFA include the following. * Identifiers (variables). * Literals, e.g., `true`, `false` (Bool), `0`, `123` (integer), `4 % 5` (rational). - * Array literals can be given by listing the key-value pairs and the (mandatory) default element, e.g., `[0 <- 182, 1 <- 41, default <- 75]`. If there are no elements, the key type has to be given before the default element, e.g., `[default <- 75]`. + * Array literals can be given by listing the key-value pairs and the (mandatory) default element, e.g., `[0 <- 182, 1 <- 41, default <- 75]`. If there are no elements, the key type has to be given before the default element, e.g., `[default <- 75]`. Note that any expression can be used as a value, but this will only result in an ArrayLitExpr when all operands are literals, or can be simplified to literals. Otherwise, this construct will yield an `ArrayInitExpr`, which is semantically equivalent to successive writes to an otherwise empty array, containing only the _else_ value for every index. * Bitvector literals can be given by stating the length and the exact value of the bitvector in binary, decimal or hexadecimal form. (E.g. `4'd5` is a 4-bit-long bitvector with the decimal value 5.) _This is an experimental feature. See the [details](doc/bitvectors.md) for more information._ * Floating point literals can be given in the following form: `[+-]?bitvector.bitvector`, defining the optional sign (+/-), exponent and significand in this order. (E.g. `+5'b10000.10'd0` is `+2.0f` of type `fp[5:11]` (half-precision IEEE-754 float)). The value is calculated the following way (using `e` for exponent size, and `E`, `S` for values, `h` for sign): `value = (-1)^h * 1.S * 2^(E-2^(e-1)+1)` * Comparison, e.g., `=`, `/=`, `<`, `>`, `<=`, `>=`. diff --git a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java index 6275664a77..6ffe416e3c 100644 --- a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java +++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java @@ -96,7 +96,7 @@ import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Rem; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Sub; import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime; -import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.ArrayInit; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; @@ -125,6 +125,7 @@ import static hu.bme.mit.theta.core.type.fptype.FpExprs.ToFp; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; +import static hu.bme.mit.theta.core.utils.ExprUtils.simplify; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; import static hu.bme.mit.theta.core.utils.TypeUtils.castBv; import static java.util.stream.Collectors.toList; @@ -1030,7 +1031,7 @@ private Expr createArrayLitExpr(final ArrL } valueType = (T2) ctx.elseExpr.accept(this).getType(); - final List, ? extends Expr>> elems = IntStream + final List, Expr>> elems = IntStream .range(0, ctx.indexExpr.size()) .mapToObj(i -> Tuple2.of( cast(ctx.indexExpr.get(i).accept(this), indexType), @@ -1039,7 +1040,7 @@ private Expr createArrayLitExpr(final ArrL .collect(Collectors.toUnmodifiableList()); final Expr elseExpr = cast(ctx.elseExpr.accept(this), valueType); - return Array(elems, elseExpr, ArrayType.of(indexType, valueType)); + return simplify(ArrayInit(elems, elseExpr, ArrayType.of(indexType, valueType))); } @Override diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java index b45ebf9087..93ef1641f9 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java @@ -2,19 +2,22 @@ import com.google.common.collect.ImmutableList; import hu.bme.mit.theta.common.Tuple2; -import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.LitExpr; -import hu.bme.mit.theta.core.type.NullaryExpr; +import hu.bme.mit.theta.core.type.MultiaryExpr; import hu.bme.mit.theta.core.type.Type; +import java.util.ArrayList; import java.util.List; import java.util.stream.Collectors; +import java.util.stream.Stream; +import java.util.stream.StreamSupport; import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; -public final class ArrayInitExpr extends NullaryExpr> { +public final class ArrayInitExpr extends MultiaryExpr> { private static final int HASH_SEED = 241; private static final String OPERATOR_LABEL = "arrayinit"; @@ -29,6 +32,8 @@ public final class ArrayInitExpr private ArrayInitExpr(final List, Expr>> elems, final Expr elseElem, final ArrayType type) { + //noinspection unchecked + super(Stream.concat(List.of((Expr)elseElem).stream(), Stream.concat(elems.stream().map(objects -> (Expr)objects.get1()), elems.stream().map(objects -> (Expr)objects.get2()))).collect(Collectors.toList())); this.type = checkNotNull(type); this.elseElem = checkNotNull(elseElem); this.elems = checkNotNull(elems); @@ -55,19 +60,6 @@ public LitExpr> eval(final Valuation val) { return ArrayLitExpr.of(elems.stream().map(objects -> Tuple2.of(objects.get1().eval(val), objects.get2().eval(val))).collect(Collectors.toList()), elseElem, type); } - @Override - public int hashCode() { - int tmp = hashCode; - if (tmp == 0) { - tmp = HASH_SEED; - tmp = 31 * tmp + type.hashCode(); - for(Tuple2, Expr> elem : elems) { - tmp = 31 * tmp + elem.hashCode(); - } - hashCode = tmp; - } - return tmp; - } @Override public boolean equals(final Object obj) { @@ -81,12 +73,36 @@ public boolean equals(final Object obj) { } } + + @SuppressWarnings("unchecked") @Override - public String toString() { - return Utils.lispStringBuilder(OPERATOR_LABEL) - .addAll(elems.stream().map(elem -> String.format("(%s %s)", elem.get1(), elem.get2()))) - .add((String.format("(default %s)", elseElem))) - .toString(); + public MultiaryExpr> with(Iterable> ops) { + long size = StreamSupport.stream(ops.spliterator(), false).count(); + checkState(size % 2 == 1, "Ops must be odd long!"); + long counter = 0; + Expr elseElem = null; + List> indices = new ArrayList<>(); + List> elems = new ArrayList<>(); + for (Expr op : ops) { + if(counter == 0) elseElem = (Expr) op; + else if (counter <= (size-1)/2) indices.add((Expr) op); + else elems.add((Expr) op); + ++counter; + } + List, Expr>> newOps = new ArrayList<>(); + for (int i = 0; i < indices.size(); i++) { + newOps.add(Tuple2.of(indices.get(i), elems.get(i))); + } + return ArrayInitExpr.of(newOps, elseElem, type); } + @Override + protected int getHashSeed() { + return HASH_SEED; + } + + @Override + public String getOperatorLabel() { + return OPERATOR_LABEL; + } } From 6d2db6012b697b4f50963370c785bc7c63735fb6 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 5 Aug 2021 23:14:57 +0200 Subject: [PATCH 10/17] Added helper comment to avoid confusion --- .../bme/mit/theta/core/type/arraytype/ArrayInitExpr.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java index 93ef1641f9..47e0f517fe 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java @@ -17,6 +17,13 @@ import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Preconditions.checkState; +/** + * ArrayInitExpr is a way to specify arbitrary array 'literals' that may contain non-literal elements as well. + * Note that while this class is a descendant of MultiaryExpr, it is used in a non-standard way: ops is only used as a + * generic Type type, and they are solely used for inter-object interactions, intra-class the `elems` and `elseElem` + * is used. These are mapped to `ops` by first placing the `elseElem`, then all indices, then all elements. + */ + public final class ArrayInitExpr extends MultiaryExpr> { private static final int HASH_SEED = 241; From 341fb1985f09805ebf9624fd341917c54ffb7f06 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 5 Aug 2021 23:18:57 +0200 Subject: [PATCH 11/17] Removed unused variable --- .../hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java index 47e0f517fe..da911b1075 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java @@ -35,8 +35,6 @@ public final class ArrayInitExpr private final Expr elseElem; - private volatile int hashCode; - private ArrayInitExpr(final List, Expr>> elems, final Expr elseElem, final ArrayType type) { //noinspection unchecked From f11fb3c91c97cfba9d639b8a33d01261ffc7388b Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 5 Aug 2021 23:20:12 +0200 Subject: [PATCH 12/17] Renamed variable to a more sensible name --- .../test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java | 2 +- .../cfa/cfa-analysis/src/test/resources/arrayinit.cfa | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java index b6374b90a5..25935c9a41 100644 --- a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java +++ b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java @@ -98,7 +98,7 @@ public static Collection data() { { "src/test/resources/arrays.cfa", PRED_BOOL, BW_BIN_ITP, false, 8 }, - { "src/test/resources/arrayinit.cfa", PRED_CART, BW_BIN_ITP, false, 4 }, + { "src/test/resources/arrayinit.cfa", PRED_CART, BW_BIN_ITP, false, 3 }, { "src/test/resources/arrays.cfa", EXPL, SEQ_ITP, false, 8 }, diff --git a/subprojects/cfa/cfa-analysis/src/test/resources/arrayinit.cfa b/subprojects/cfa/cfa-analysis/src/test/resources/arrayinit.cfa index 6a3f753246..099aa9e81b 100644 --- a/subprojects/cfa/cfa-analysis/src/test/resources/arrayinit.cfa +++ b/subprojects/cfa/cfa-analysis/src/test/resources/arrayinit.cfa @@ -1,16 +1,14 @@ main process cfa { var arr: [int]->int - var asd: int + var x: int init loc L0 - loc L01 loc L1 loc L2 final loc END error loc ERR - L0 -> L01 { asd := 1} - L01 -> L1 { arr := [ 0 <- 1, 1 <- asd + 2, default <- 0 ] } + L0 -> L1 { arr := [ 0 <- 1, 1 <- x + 2, default <- 0 ] } L1 -> L2 { assume arr[0] = 1 and arr[34] = 0 } L1 -> ERR { assume not (arr[0] = 1 and arr[34] = 0) } From 2dfbd9bfddcee81ea0bbdae47b40b9378c102d71 Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Thu, 5 Aug 2021 23:28:51 +0200 Subject: [PATCH 13/17] Added comment to simplifyGenericArrayRead --- .../main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index 14f1fb59b6..cbe0a93b0b 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java @@ -415,7 +415,7 @@ private static Expr simplifyArrayRead(final ArrayReadExpr expr, final V simplifyGenericArrayRead(final ArrayReadExpr expr, final Valuation val) { Expr> arr = simplify(expr.getArray(), val); Expr index = simplify(expr.getIndex(), val); - if (arr instanceof LitExpr && index instanceof LitExpr) { + if (arr instanceof LitExpr && index instanceof LitExpr) { //The index is required to be a literal so that we can use 'equals' to compare it against existing keys in the array return expr.eval(val); } return expr.with(arr, index); From b95977944e102b8dc482a8b084681f2add509f89 Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Sat, 7 Aug 2021 15:25:17 +0200 Subject: [PATCH 14/17] Cleaned up formatting in comment --- .../bme/mit/theta/core/type/arraytype/ArrayInitExpr.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java index da911b1075..975ff0a072 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayInitExpr.java @@ -19,9 +19,10 @@ /** * ArrayInitExpr is a way to specify arbitrary array 'literals' that may contain non-literal elements as well. - * Note that while this class is a descendant of MultiaryExpr, it is used in a non-standard way: ops is only used as a - * generic Type type, and they are solely used for inter-object interactions, intra-class the `elems` and `elseElem` - * is used. These are mapped to `ops` by first placing the `elseElem`, then all indices, then all elements. + * Note that while this class is a descendant of MultiaryExpr, it is used in a non-standard way: + * - ops is only used as a generic Type type, + * - ops are solely used for inter-object interactions, intra-class the `elems` and `elseElem` are used. + * - `elems` and `elseElem` are mapped to `ops` by first placing the `elseElem`, then all indices, then all elements. */ public final class ArrayInitExpr extends MultiaryExpr> { From a0c9ff9bd4e0ceff63334221ccf6d117a7ac2464 Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Sat, 7 Aug 2021 15:28:05 +0200 Subject: [PATCH 15/17] Fixed formatting --- .../hu/bme/mit/theta/solver/z3/Z3SolverTest.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/subprojects/common/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java b/subprojects/common/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java index e9a2517f35..c4b6651c86 100644 --- a/subprojects/common/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java +++ b/subprojects/common/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java @@ -157,7 +157,7 @@ public void testArray() { @Test public void testArrayInit() { - final ConstDecl> arr = Const("arr", Array(Int(), Int())); + final ConstDecl> arr = Const("arr", Array(Int(), Int())); var elems = new ArrayList, Expr>>(); ConstDecl noname = Const("noname", Int()); elems.add(Tuple2.of(Int(0), Int(1))); @@ -165,19 +165,19 @@ public void testArrayInit() { elems.add(Tuple2.of(Int(2), Add(noname.getRef(), Int(3)))); var initarr = ArrayInit(elems, Int(100), Array(Int(), Int())); - solver.add(ArrayExprs.Eq(arr.getRef(), initarr)); + solver.add(ArrayExprs.Eq(arr.getRef(), initarr)); - // Check, the expression should be satisfiable - SolverStatus status = solver.check(); - assertTrue(status.isSat()); + // Check, the expression should be satisfiable + SolverStatus status = solver.check(); + assertTrue(status.isSat()); solver.add(Eq(noname.getRef(), Int(1))); status = solver.check(); assertTrue(status.isSat()); Valuation valuation = solver.getModel(); - final Optional>> optVal = valuation.eval(arr); - assertTrue(optVal.isPresent()); + final Optional>> optVal = valuation.eval(arr); + assertTrue(optVal.isPresent()); final Expr> val = optVal.get(); assertTrue(val instanceof ArrayLitExpr); var valLit = (ArrayLitExpr)val; From c81108dccfd8e3799c058554e36360f6e7fabfaa Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Sat, 7 Aug 2021 15:30:44 +0200 Subject: [PATCH 16/17] Added simplification test for ArrayInitExpr -> ArrayLitExpr --- .../java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java index 2b2de34a11..6e5e8d5f54 100644 --- a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java +++ b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java @@ -756,6 +756,10 @@ public void testArrayInit() { var elems = new ArrayList, Expr>>(); elems.add(Tuple2.of(Int(0), Int(1))); elems.add(Tuple2.of(Int(1), Add(Int(1), Int(2)))); + var initArr = ArrayInit(elems, Int(100), Array(Int(), Int())); + var litArr = simplify(initArr); + assertTrue(litArr instanceof ArrayLitExpr); + VarDecl noname = Var("noname", Int()); elems.add(Tuple2.of(Int(2), Add(noname.getRef(), Int(1)))); var arr = ArrayInit(elems, Int(100), Array(Int(), Int())); From 44381d8b8da9743d7be225a15d898d4f98329630 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sat, 7 Aug 2021 22:42:11 +0200 Subject: [PATCH 17/17] bump minor version number --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index 3d56a210ea..855fd80a40 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -10,7 +10,7 @@ buildscript { allprojects { group = "hu.bme.mit.inf.theta" - version = "2.20.0" + version = "2.21.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) }