diff --git a/.github/actions/build-archive/action.yml b/.github/actions/build-archive/action.yml index c6afb0bfa2..d042b3826d 100644 --- a/.github/actions/build-archive/action.yml +++ b/.github/actions/build-archive/action.yml @@ -17,23 +17,23 @@ runs: - name: Create folder structure shell: bash run: | - mkdir -p ${{ inputs.name }}/theta/ - mkdir -p ${{ inputs.name }}/theta/solvers - cp lib ${{ inputs.name }}/theta/lib -r - cp CONTRIBUTORS.md ${{ inputs.name }}/theta/ - cp lib/README.md ${{ inputs.name }}/theta/LIB_LICENSES.md - cp LICENSE ${{ inputs.name }}/theta/ - cp README.md ${{ inputs.name }}/theta/GENERAL_README.md - cp scripts/theta-start.sh ${{ inputs.name }}/theta/theta-start.sh - chmod +x ${{ inputs.name }}/theta/theta-start.sh - sed "s/COMMIT_ID/$GITHUB_SHA/g" $GITHUB_ACTION_PATH/README.md > ${{ inputs.name }}/theta/README.md - sed -i 's/TOOL_NAME/${{ inputs.name }}/g' ${{ inputs.name }}/theta/README.md - sed -i 's/INPUT_FLAG/${{ inputs.inputflag }}/g' ${{ inputs.name }}/theta/README.md + mkdir -p ${{ inputs.name }}/${{ inputs.name }}/ + mkdir -p ${{ inputs.name }}/${{ inputs.name }}/solvers + cp lib ${{ inputs.name }}/${{ inputs.name }}/lib -r + cp CONTRIBUTORS.md ${{ inputs.name }}/${{ inputs.name }}/ + cp lib/README.md ${{ inputs.name }}/${{ inputs.name }}/LIB_LICENSES.md + cp LICENSE ${{ inputs.name }}/${{ inputs.name }}/ + cp README.md ${{ inputs.name }}/${{ inputs.name }}/GENERAL_README.md + cp scripts/theta-start.sh ${{ inputs.name }}/${{ inputs.name }}/theta-start.sh + chmod +x ${{ inputs.name }}/${{ inputs.name }}/theta-start.sh + sed "s/COMMIT_ID/$GITHUB_SHA/g" $GITHUB_ACTION_PATH/README.md > ${{ inputs.name }}/${{ inputs.name }}/README.md + sed -i 's/TOOL_NAME/${{ inputs.name }}/g' ${{ inputs.name }}/${{ inputs.name }}/README.md + sed -i 's/INPUT_FLAG/${{ inputs.inputflag }}/g' ${{ inputs.name }}/${{ inputs.name }}/README.md - name: Extract theta-xcfa-cli and theta-smtlib-cli shell: bash run: | - mv jar/xcfa/xcfa-cli/build/libs/*-all.jar ${{ inputs.name }}/theta/theta.jar - mv jar/solver/solver-smtlib-cli/build/libs/*-all.jar ${{ inputs.name }}/theta/theta-smtlib.jar + mv jar/xcfa/xcfa-cli/build/libs/*-all.jar ${{ inputs.name }}/${{ inputs.name }}/theta.jar + mv jar/solver/solver-smtlib-cli/build/libs/*-all.jar ${{ inputs.name }}/${{ inputs.name }}/theta-smtlib.jar - name: Setup java 17 uses: actions/setup-java@5ffc13f4174014e2d4d4572b3d74c3fa61aeb2c2 # v3.11.0 with: @@ -44,15 +44,15 @@ runs: run: | for i in $(cat $GITHUB_ACTION_PATH/necessary-solvers.txt) do - java -jar ${{ inputs.name }}/theta/theta-smtlib.jar --home ${{ inputs.name }}/theta/solvers install $i + java -jar ${{ inputs.name }}/${{ inputs.name }}/theta-smtlib.jar --home ${{ inputs.name }}/${{ inputs.name }}/solvers install $i done - name: ZIP archive shell: bash run: | cd ${{ inputs.name }} - zip theta.zip theta -r + zip ${{ inputs.name }}.zip ${{ inputs.name }} -r - name: Upload results uses: actions/upload-artifact@0b7f8abb1508181956e8e162db84b466c27e18ce # v3.1.2 with: name: ${{ inputs.name }}_SV-COMP - path: ${{ inputs.name }}/theta.zip + path: ${{ inputs.name }}/${{ inputs.name }}.zip 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 c1d40d8d54..25e8fed126 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 @@ -64,6 +64,7 @@ import hu.bme.mit.theta.core.type.bvtype.BvSModExpr; import hu.bme.mit.theta.core.type.bvtype.BvSRemExpr; import hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSignChangeExpr; import hu.bme.mit.theta.core.type.bvtype.BvSubExpr; import hu.bme.mit.theta.core.type.bvtype.BvUDivExpr; import hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr; @@ -255,6 +256,8 @@ private ExprWriter() { .addCase(BvPosExpr.class, e -> prefixUnary(e, "bvpos")) + .addCase(BvSignChangeExpr.class, e -> prefixUnary(e, "bvsign")) + .addCase(BvNegExpr.class, e -> prefixUnary(e, "bvneg")) .addCase(BvAndExpr.class, e -> infixMultiary(e, " bvand ")) diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvSignChangeExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvSignChangeExpr.java new file mode 100644 index 0000000000..d7a65d7a12 --- /dev/null +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvSignChangeExpr.java @@ -0,0 +1,88 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.core.type.bvtype; + +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.abstracttype.PosExpr; + +import static hu.bme.mit.theta.core.utils.TypeUtils.castBv; + +public final class BvSignChangeExpr extends PosExpr { + + private static final int HASH_SEED = 8963; + private static final String OPERATOR_LABEL = "bvpos"; + + private final BvType newType; + + private BvSignChangeExpr(final Expr op, final BvType newType) { + super(op); + this.newType = newType; + } + + public static BvSignChangeExpr of(final Expr op, final BvType newType) { + return new BvSignChangeExpr(op, newType); + } + + public static BvSignChangeExpr create(final Expr op, final BvType newType) { + final Expr newOp = castBv(op); + return BvSignChangeExpr.of(newOp, newType); + } + + @Override + public BvType getType() { + return newType; + } + + @Override + public BvLitExpr eval(final Valuation val) { + final BvLitExpr opVal = (BvLitExpr) getOp().eval(val); + return opVal.pos(); + } + + @Override + public BvSignChangeExpr with(final Expr op) { + if (op == getOp()) { + return this; + } else { + return BvSignChangeExpr.of(op, newType); + } + } + + @Override + public boolean equals(final Object obj) { + if (this == obj) { + return true; + } else if (obj != null && this.getClass() == obj.getClass()) { + final BvSignChangeExpr that = (BvSignChangeExpr) obj; + return this.getOp().equals(that.getOp()) && this.getType().equals(that.getType()); + } else { + return false; + } + } + + @Override + protected int getHashSeed() { + return HASH_SEED; + } + + @Override + public String getOperatorLabel() { + return OPERATOR_LABEL; + } + +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprCanonizer.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprCanonizer.java index 17a1248a38..5baebf0284 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprCanonizer.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprCanonizer.java @@ -16,23 +16,94 @@ package hu.bme.mit.theta.core.utils; import hu.bme.mit.theta.common.DispatchTable; -import hu.bme.mit.theta.common.Utils; -import hu.bme.mit.theta.core.model.Valuation; -import hu.bme.mit.theta.core.type.*; +import hu.bme.mit.theta.core.type.BinaryExpr; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.MultiaryExpr; +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.ArrayReadExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr; -import hu.bme.mit.theta.core.type.booltype.*; -import hu.bme.mit.theta.core.type.bvtype.*; -import hu.bme.mit.theta.core.type.inttype.*; -import hu.bme.mit.theta.core.type.rattype.*; - -import java.util.*; +import hu.bme.mit.theta.core.type.booltype.AndExpr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.booltype.IffExpr; +import hu.bme.mit.theta.core.type.booltype.ImplyExpr; +import hu.bme.mit.theta.core.type.booltype.NotExpr; +import hu.bme.mit.theta.core.type.booltype.OrExpr; +import hu.bme.mit.theta.core.type.booltype.XorExpr; +import hu.bme.mit.theta.core.type.bvtype.BvAddExpr; +import hu.bme.mit.theta.core.type.bvtype.BvAndExpr; +import hu.bme.mit.theta.core.type.bvtype.BvArithShiftRightExpr; +import hu.bme.mit.theta.core.type.bvtype.BvConcatExpr; +import hu.bme.mit.theta.core.type.bvtype.BvEqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvExtractExpr; +import hu.bme.mit.theta.core.type.bvtype.BvLogicShiftRightExpr; +import hu.bme.mit.theta.core.type.bvtype.BvMulExpr; +import hu.bme.mit.theta.core.type.bvtype.BvNegExpr; +import hu.bme.mit.theta.core.type.bvtype.BvNeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvNotExpr; +import hu.bme.mit.theta.core.type.bvtype.BvOrExpr; +import hu.bme.mit.theta.core.type.bvtype.BvPosExpr; +import hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr; +import hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSDivExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSExtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSGeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSGtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSLeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSLtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSModExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSRemExpr; +import hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSignChangeExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSubExpr; +import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.bvtype.BvUDivExpr; +import hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvUGtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvULeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvULtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvURemExpr; +import hu.bme.mit.theta.core.type.bvtype.BvXorExpr; +import hu.bme.mit.theta.core.type.bvtype.BvZExtExpr; +import hu.bme.mit.theta.core.type.inttype.IntAddExpr; +import hu.bme.mit.theta.core.type.inttype.IntDivExpr; +import hu.bme.mit.theta.core.type.inttype.IntEqExpr; +import hu.bme.mit.theta.core.type.inttype.IntExprs; +import hu.bme.mit.theta.core.type.inttype.IntGeqExpr; +import hu.bme.mit.theta.core.type.inttype.IntGtExpr; +import hu.bme.mit.theta.core.type.inttype.IntLeqExpr; +import hu.bme.mit.theta.core.type.inttype.IntLtExpr; +import hu.bme.mit.theta.core.type.inttype.IntModExpr; +import hu.bme.mit.theta.core.type.inttype.IntMulExpr; +import hu.bme.mit.theta.core.type.inttype.IntNegExpr; +import hu.bme.mit.theta.core.type.inttype.IntNeqExpr; +import hu.bme.mit.theta.core.type.inttype.IntPosExpr; +import hu.bme.mit.theta.core.type.inttype.IntSubExpr; +import hu.bme.mit.theta.core.type.inttype.IntToRatExpr; +import hu.bme.mit.theta.core.type.inttype.IntType; +import hu.bme.mit.theta.core.type.rattype.RatAddExpr; +import hu.bme.mit.theta.core.type.rattype.RatDivExpr; +import hu.bme.mit.theta.core.type.rattype.RatEqExpr; +import hu.bme.mit.theta.core.type.rattype.RatExprs; +import hu.bme.mit.theta.core.type.rattype.RatGeqExpr; +import hu.bme.mit.theta.core.type.rattype.RatGtExpr; +import hu.bme.mit.theta.core.type.rattype.RatLeqExpr; +import hu.bme.mit.theta.core.type.rattype.RatLtExpr; +import hu.bme.mit.theta.core.type.rattype.RatMulExpr; +import hu.bme.mit.theta.core.type.rattype.RatNegExpr; +import hu.bme.mit.theta.core.type.rattype.RatNeqExpr; +import hu.bme.mit.theta.core.type.rattype.RatPosExpr; +import hu.bme.mit.theta.core.type.rattype.RatSubExpr; +import hu.bme.mit.theta.core.type.rattype.RatToIntExpr; +import hu.bme.mit.theta.core.type.rattype.RatType; + +import java.util.Comparator; +import java.util.List; import java.util.stream.Collectors; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; public final class ExprCanonizer { @@ -132,6 +203,8 @@ public final class ExprCanonizer { .addCase(BvPosExpr.class, ExprCanonizer::canonizeBvPos) + .addCase(BvSignChangeExpr.class, ExprCanonizer::canonizeBvSignChange) + .addCase(BvNegExpr.class, ExprCanonizer::canonizeBvNeg) .addCase(BvMulExpr.class, ExprCanonizer::canonizeBvMul) @@ -502,6 +575,10 @@ private static Expr canonizeBvPos(final BvPosExpr expr) { throw new UnsupportedOperationException(); } + private static Expr canonizeBvSignChange(final BvSignChangeExpr expr) { + throw new UnsupportedOperationException(); + } + private static Expr canonizeBvNeg(final BvNegExpr expr) { throw new UnsupportedOperationException(); } 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 a42549b81b..59a7bd3b80 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 @@ -63,6 +63,7 @@ import hu.bme.mit.theta.core.type.bvtype.BvSModExpr; import hu.bme.mit.theta.core.type.bvtype.BvSRemExpr; import hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSignChangeExpr; import hu.bme.mit.theta.core.type.bvtype.BvSubExpr; import hu.bme.mit.theta.core.type.bvtype.BvType; import hu.bme.mit.theta.core.type.bvtype.BvUDivExpr; @@ -264,6 +265,8 @@ public static ExprSimplifier create(final SimplifierLevel level) { .addCase(BvPosExpr.class, this::simplifyBvPos) + .addCase(BvSignChangeExpr.class, this::simplifyBvSignChange) + .addCase(BvNegExpr.class, this::simplifyBvNeg) .addCase(BvMulExpr.class, this::simplifyBvMul) @@ -1286,6 +1289,10 @@ private Expr simplifyBvPos(final BvPosExpr expr, final Valuation val) { return simplify(expr.getOp(), val); } + private Expr simplifyBvSignChange(final BvSignChangeExpr expr, final Valuation val) { + return simplify(expr.getOp(), val); + } + private Expr simplifyBvNeg(final BvNegExpr expr, final Valuation val) { final Expr op = simplify(expr.getOp(), val); diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index 20f9b83a98..920a9e9456 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -445,14 +445,15 @@ private Expr createIntDiv(Expr a, Expr b) { */ private Expr createIntMod(Expr a, Expr b) { ModExpr aModB = Mod(a, b); - return Ite(Geq(a, Int(0)), // if (a >= 0) - aModB, // a mod b - // else - Ite(Geq(b, Int(0)), // if (b >= 0) - Sub(aModB, b), // a mod b - b - Add(aModB, b) // a mod b + b - ) - ); + return Ite(Eq(aModB, Int(0)), aModB, + Ite(Geq(a, Int(0)), // if (a >= 0) + aModB, // a mod b + // else + Ite(Geq(b, Int(0)), // if (b >= 0) + Sub(aModB, b), // a mod b - b + Add(aModB, b) // a mod b + b + ) + )); } @Override @@ -484,7 +485,7 @@ public Expr visitUnaryExpressionSizeOrAlignOf(CParser.UnaryExpressionSizeOrAl .or(() -> Optional.ofNullable(CComplexType.getType(getVar(ctx.typeName().getText()).getRef(), parseContext))); if (type.isPresent()) { - LitExpr value = CComplexType.getSignedInt(parseContext).getValue("" + parseContext.getArchitecture().getBitWidth(type.get().getTypeName()) / 8); + LitExpr value = CComplexType.getSignedInt(parseContext).getValue("" + type.get().width() / 8); return value; } else { uniqueWarningLogger.write(Level.INFO, "WARNING: sizeof got unknown type, using a literal 0 instead.\n"); diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/preprocess/ArithmeticTrait.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/preprocess/ArithmeticTrait.java index 97c233ea58..7941bbe4d8 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/preprocess/ArithmeticTrait.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/preprocess/ArithmeticTrait.java @@ -17,5 +17,5 @@ package hu.bme.mit.theta.frontend.transformation.grammar.preprocess; public enum ArithmeticTrait { - LIN_INT, NONLIN_INT, BITWISE, FLOAT, ARR, + LIN_INT, NONLIN_INT, BITWISE, FLOAT, ARR, MULTITHREAD } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java index 8d4bbb8393..0a7fae1acb 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java @@ -160,7 +160,7 @@ public static CComplexType getType(String s, ParseContext parseContext) { if (s.endsWith("*")) { yield new CPointer(null, null, parseContext); } else { - throw new RuntimeException("Type not known: " + s); + yield null; } } }; diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/compound/CCompound.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/compound/CCompound.java index 54746c38b0..815fe8b196 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/compound/CCompound.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/compound/CCompound.java @@ -30,4 +30,8 @@ public R accept(CComplexTypeVisitor visitor, T param) { return visitor.visit(this, param); } + @Override + public int width() { + return parseContext.getArchitecture().getBitWidth("int"); + } } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CReal.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CReal.java index af822e83ed..a29b8d8282 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CReal.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/real/CReal.java @@ -32,6 +32,12 @@ public R accept(CComplexTypeVisitor visitor, T param) { return visitor.visit(this, param); } + @Override + public int width() { + return parseContext.getArchitecture().getBitWidth(getTypeName() + "_s") + + parseContext.getArchitecture().getBitWidth(getTypeName() + "_e"); + } + @Override public CComplexType getSmallestCommonType(CComplexType type) { if (!(type instanceof CReal) || ((CReal) type).rank <= rank) { diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/bitvector/CastVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/bitvector/CastVisitor.java index 200c5b7486..86466077c1 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/bitvector/CastVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/bitvector/CastVisitor.java @@ -19,6 +19,7 @@ import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.bvtype.BvExprs; +import hu.bme.mit.theta.core.type.bvtype.BvSignChangeExpr; import hu.bme.mit.theta.core.type.bvtype.BvType; import hu.bme.mit.theta.core.type.fptype.FpExprs; import hu.bme.mit.theta.core.type.fptype.FpRoundingMode; @@ -84,8 +85,12 @@ private Expr handleSignedConversion(CInteger type, Expr param } else if (that.width() > type.width()) { return BvExprs.Extract(cast(param, BvType.of(that.width())), Int(0), Int(type.width())); - } else { - return BvExprs.Pos((Expr) param); + } else { // width equals + if (that instanceof Unsigned) { + return BvSignChangeExpr.of((Expr) param, BvType.of(((BvType) param.getType()).getSize(), true)); + } else { + return param; + } } } else { throw new IllegalStateException("Compound types are not directly supported!"); @@ -113,7 +118,7 @@ private Expr handleUnsignedConversion(CInteger type, Expr par Int(type.width())); } else { // width equals if (that instanceof Signed) { - return BvExprs.Add(List.of((Expr) param, BvUtils.bigIntegerToUnsignedBvLitExpr(BigInteger.TWO.pow(type.width()).subtract(BigInteger.ONE), type.width()), (Expr) type.getUnitValue())); + return BvSignChangeExpr.of((Expr) param, BvType.of(((BvType) param.getType()).getSize(), false)); } else { return param; } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/integer/CastVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/integer/CastVisitor.java index bfb6633ffd..312a47ffad 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/integer/CastVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/integer/CastVisitor.java @@ -192,7 +192,12 @@ public Expr visit(CUnsignedChar type, Expr param) { @Override public Expr visit(CBool type, Expr param) { - return Ite(Eq(param, Int(0)), Int(0), Int(1)); + CComplexType that = CComplexType.getType(param, parseContext); + if (that instanceof CBool) { + return param; + } else { + return Ite(Eq(param, Int(0)), Int(0), Int(1)); + } } @Override diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java index b3d4f53053..4e5b8bcef8 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java @@ -71,6 +71,7 @@ import hu.bme.mit.theta.core.type.bvtype.BvSModExpr; import hu.bme.mit.theta.core.type.bvtype.BvSRemExpr; import hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSignChangeExpr; import hu.bme.mit.theta.core.type.bvtype.BvSubExpr; import hu.bme.mit.theta.core.type.bvtype.BvUDivExpr; import hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr; @@ -274,6 +275,8 @@ public GenericSmtLibExprTransformer(final SmtLibTransformationManager transforme .addCase(BvPosExpr.class, this::transformBvPos) + .addCase(BvSignChangeExpr.class, this::transformBvSignChange) + .addCase(BvNegExpr.class, this::transformBvNeg) .addCase(BvMulExpr.class, this::transformBvMul) @@ -773,6 +776,10 @@ protected String transformBvPos(final BvPosExpr expr) { return toTerm(expr.getOp()); } + protected String transformBvSignChange(final BvSignChangeExpr expr) { + return toTerm(expr.getOp()); + } + protected String transformBvNeg(final BvNegExpr expr) { return String.format("(bvneg %s)", toTerm(expr.getOp())); } diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java index 31991d0f95..2f5e5c9886 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java @@ -414,7 +414,7 @@ protected Expr transformTerm(final TermContext ctx, final SmtLibModel model, } else if (ctx.exists_term() != null) { return transformExistsTerm(ctx.exists_term(), model, vars); } else if (ctx.match_term() != null) { - throw new UnsupportedOperationException(); + throw new SmtLibSolverException(""); } else if (ctx.annotate_term() != null) { return transformTerm(ctx.annotate_term().term(), model, vars); } else { @@ -436,7 +436,7 @@ protected Expr transformSpecConstant(final Spec_constantContext ctx, final Sm } else if (ctx.binary() != null) { return transformBinary(ctx.binary(), model, vars); } else if (ctx.string() != null) { - throw new UnsupportedOperationException(); + throw new SmtLibSolverException(""); } else { throw new SmtLibSolverException("Invalid input"); } @@ -469,7 +469,7 @@ protected Expr transformGenericTerm(final Generic_termContext ctx, final SmtL final var expr = transformTerm(funAppParams.get(0), model, vars); return createArrayLitExpr(expr, arrayType); } else { - throw new UnsupportedOperationException(); + throw new SmtLibSolverException(""); } } else if (funAppTransformer.containsKey(funName)) { // known function application return funAppTransformer.get(funName).apply(funParams, funAppParams, model, vars); @@ -619,7 +619,7 @@ protected Expr transformSymbol(final SymbolContext ctx, final SmtLibModel mod } else if (symbolTable.definesSymbol(value)) { return symbolTable.getConst(value).getRef(); } else { - throw new UnsupportedOperationException(); + throw new SmtLibSolverException("Transforation of symbol not supported: " + value); } } } @@ -681,7 +681,7 @@ protected Type transformSort(final SortContext ctx) { assert ctx.sort().size() == 2; return Array(transformSort(ctx.sort().get(0)), transformSort(ctx.sort().get(1))); default: - throw new UnsupportedOperationException(); + throw new SmtLibSolverException(""); } } @@ -903,7 +903,7 @@ private FpRoundingMode fpOperatorRoundingMode(final TermContext term) { case "RTZ": return FpRoundingMode.RTZ; default: - throw new UnsupportedOperationException(); + throw new SmtLibSolverException(""); } } diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java index dacf64971c..a337801d55 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java @@ -75,6 +75,7 @@ import hu.bme.mit.theta.core.type.bvtype.BvSModExpr; import hu.bme.mit.theta.core.type.bvtype.BvSRemExpr; import hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSignChangeExpr; import hu.bme.mit.theta.core.type.bvtype.BvSubExpr; import hu.bme.mit.theta.core.type.bvtype.BvUDivExpr; import hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr; @@ -278,6 +279,8 @@ public Z3ExprTransformer(final Z3TransformationManager transformer, final Contex .addCase(BvPosExpr.class, this::transformBvPos) + .addCase(BvSignChangeExpr.class, this::transformBvSignChange) + .addCase(BvNegExpr.class, this::transformBvNeg) .addCase(BvMulExpr.class, this::transformBvMul) @@ -824,6 +827,10 @@ private com.microsoft.z3.Expr transformBvPos(final BvPosExpr expr) { return toTerm(expr.getOp()); } + private com.microsoft.z3.Expr transformBvSignChange(final BvSignChangeExpr expr) { + return toTerm(expr.getOp()); + } + private com.microsoft.z3.Expr transformBvNeg(final BvNegExpr expr) { final BitVecExpr opTerm = (BitVecExpr) toTerm(expr.getOp()); return context.mkBVNeg(opTerm); diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt index 5931d24699..bf3b1772cf 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt @@ -640,19 +640,20 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo val breakLoc = param.breakLoc val continueLoc = param.continueLoc val returnLoc = param.returnLoc - val expr = statement.expr ?: return lastLoc + val expr = statement.expr val initLoc = getLoc(builder, statement.id, metadata = getMetadata(statement)) builder.addLoc(initLoc) val xcfaEdge: XcfaEdge = XcfaEdge(lastLoc, initLoc, metadata = getMetadata(statement)) builder.addEdge(xcfaEdge) - val endExpr = expr.accept(this, - ParamPack(builder, initLoc, breakLoc, continueLoc, returnLoc)) + val endExpr = expr?.accept(this, + ParamPack(builder, initLoc, breakLoc, continueLoc, returnLoc)) ?: initLoc val endLoc = getAnonymousLoc(builder, metadata = getMetadata(statement)) builder.addLoc(endLoc) val key: VarDecl<*> = builder.getParams()[0].first check(returnLoc != null) + val type = CComplexType.getType(key.ref, parseContext) val edge = XcfaEdge(endExpr, returnLoc, StmtLabel(Stmts.Assign(cast(key, key.type), - cast(CComplexType.getType(key.ref, parseContext).castTo(expr.expression), key.type)), + cast(type.castTo(expr?.expression ?: type.nullValue), key.type)), metadata = getMetadata(statement)), metadata = getMetadata(statement)) builder.addEdge(edge) return endLoc diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarServer.java b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarServer.java index 440b2d2d35..4e35e08e7c 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarServer.java +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarServer.java @@ -165,7 +165,7 @@ private void run(String[] args) { } catch (Exception e) { File tempFile = File.createTempFile("parsecontext", ".json"); try (BufferedWriter bw = new BufferedWriter(new FileWriter(tempFile))) { - bw.write(configStr); + bw.write(parseStr); } System.err.println("Erroneous parsecontext, see file " + tempFile.getAbsolutePath()); throw e; diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt index bdaba9c0b3..b812d15475 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt @@ -62,7 +62,7 @@ fun complexPortfolio24( ) if (traitsTyped.multithreaded) { - baseConfig = baseConfig.copy(search = Search.DFS, porLevel = POR.AASPOR, pruneStrategy = PruneStrategy.LAZY, + baseConfig = baseConfig.copy(search = Search.DFS, porLevel = POR.AASPOR, pruneStrategy = PruneStrategy.FULL, coi = ConeOfInfluenceMode.COI) if (propertyTyped == ErrorDetection.DATA_RACE) { @@ -408,6 +408,75 @@ fun complexPortfolio24( timeoutMs = 500000 ), checker, inProcess) edges.add(Edge(config_ARR_PRED_CART_SEQ_ITP_princess, config_ARR_PRED_CART_SEQ_ITP_cvc5, solverError)) + val config_MULTITHREAD_EXPL_SEQ_ITP_Z3 = ConfigNode("MULTITHREAD_EXPL_SEQ_ITP_Z3-$inProcess", baseConfig.copy( + domain = Domain.EXPL, + abstractionSolver = "Z3", + refinementSolver = "Z3", + refinement = Refinement.SEQ_ITP, + timeoutMs = 150000 + ), checker, inProcess) + val config_MULTITHREAD_EXPL_SEQ_ITP_mathsat = ConfigNode("MULTITHREAD_EXPL_SEQ_ITP_mathsat:5.6.10-$inProcess", + baseConfig.copy( + domain = Domain.EXPL, + abstractionSolver = "mathsat:5.6.10", + refinementSolver = "mathsat:5.6.10", + refinement = Refinement.SEQ_ITP, + timeoutMs = 150000 + ), checker, inProcess) + edges.add(Edge(config_MULTITHREAD_EXPL_SEQ_ITP_Z3, config_MULTITHREAD_EXPL_SEQ_ITP_mathsat, solverError)) + val config_MULTITHREAD_EXPL_NWT_IT_WP_z3 = ConfigNode("MULTITHREAD_EXPL_NWT_IT_WP_z3:4.12.2-$inProcess", + baseConfig.copy( + domain = Domain.EXPL, + abstractionSolver = "z3:4.12.2", + refinementSolver = "z3:4.12.2", + refinement = Refinement.NWT_IT_WP, + timeoutMs = 300000 + ), checker, inProcess) + edges.add(Edge(config_MULTITHREAD_EXPL_SEQ_ITP_Z3, config_MULTITHREAD_EXPL_NWT_IT_WP_z3, + if (inProcess) timeoutTrigger else anyError)) + edges.add(Edge(config_MULTITHREAD_EXPL_SEQ_ITP_mathsat, config_MULTITHREAD_EXPL_NWT_IT_WP_z3, + if (inProcess) timeoutOrSolverError else anyError)) + val config_MULTITHREAD_EXPL_NWT_IT_WP_mathsat = ConfigNode( + "MULTITHREAD_EXPL_NWT_IT_WP_mathsat:5.6.10-$inProcess", baseConfig.copy( + domain = Domain.EXPL, + abstractionSolver = "mathsat:5.6.10", + refinementSolver = "mathsat:5.6.10", + refinement = Refinement.NWT_IT_WP, + timeoutMs = 300000 + ), checker, inProcess) + edges.add(Edge(config_MULTITHREAD_EXPL_NWT_IT_WP_z3, config_MULTITHREAD_EXPL_NWT_IT_WP_mathsat, solverError)) + val config_MULTITHREAD_PRED_CART_SEQ_ITP_Z3 = ConfigNode("MULTITHREAD_PRED_CART_SEQ_ITP_Z3-$inProcess", + baseConfig.copy( + domain = Domain.PRED_CART, + abstractionSolver = "Z3", + refinementSolver = "Z3", + refinement = Refinement.SEQ_ITP, + timeoutMs = 0 + ), checker, inProcess) + edges.add(Edge(config_MULTITHREAD_EXPL_NWT_IT_WP_z3, config_MULTITHREAD_PRED_CART_SEQ_ITP_Z3, + if (inProcess) timeoutTrigger else anyError)) + edges.add(Edge(config_MULTITHREAD_EXPL_NWT_IT_WP_mathsat, config_MULTITHREAD_PRED_CART_SEQ_ITP_Z3, + if (inProcess) timeoutOrSolverError else anyError)) + val config_MULTITHREAD_PRED_CART_SEQ_ITP_mathsat = ConfigNode( + "MULTITHREAD_PRED_CART_SEQ_ITP_mathsat:5.6.10-$inProcess", baseConfig.copy( + domain = Domain.PRED_CART, + abstractionSolver = "mathsat:5.6.10", + refinementSolver = "mathsat:5.6.10", + refinement = Refinement.SEQ_ITP, + timeoutMs = 0 + ), checker, inProcess) + edges.add( + Edge(config_MULTITHREAD_PRED_CART_SEQ_ITP_Z3, config_MULTITHREAD_PRED_CART_SEQ_ITP_mathsat, solverError)) + val config_MULTITHREAD_PRED_CART_SEQ_ITP_z3 = ConfigNode("MULTITHREAD_PRED_CART_SEQ_ITP_z3:4.12.2-$inProcess", + baseConfig.copy( + domain = Domain.PRED_CART, + abstractionSolver = "z3:4.12.2", + refinementSolver = "z3:4.12.2", + refinement = Refinement.SEQ_ITP, + timeoutMs = 0 + ), checker, inProcess) + edges.add( + Edge(config_MULTITHREAD_PRED_CART_SEQ_ITP_mathsat, config_MULTITHREAD_PRED_CART_SEQ_ITP_z3, solverError)) if (trait == ArithmeticTrait.BITWISE) { return STM(config_BITWISE_EXPL_NWT_IT_WP_cvc5, edges) } @@ -428,15 +497,25 @@ fun complexPortfolio24( return STM(config_ARR_EXPL_NWT_IT_WP_cvc5, edges) } + if (trait == ArithmeticTrait.MULTITHREAD) { + return STM(config_MULTITHREAD_EXPL_SEQ_ITP_Z3, edges) + } + + error("Unknown trait!") } val mainTrait = - if (ArithmeticTrait.FLOAT in traitsTyped.arithmeticTraits) ArithmeticTrait.FLOAT - else if (ArithmeticTrait.ARR in traitsTyped.arithmeticTraits) ArithmeticTrait.ARR - else if (ArithmeticTrait.BITWISE in traitsTyped.arithmeticTraits) ArithmeticTrait.BITWISE - else if (ArithmeticTrait.NONLIN_INT in traitsTyped.arithmeticTraits) ArithmeticTrait.NONLIN_INT - else ArithmeticTrait.LIN_INT + when { + traitsTyped.multithreaded -> ArithmeticTrait.MULTITHREAD + ArithmeticTrait.FLOAT in traitsTyped.arithmeticTraits -> ArithmeticTrait.FLOAT + ArithmeticTrait.ARR in traitsTyped.arithmeticTraits -> ArithmeticTrait.ARR + ArithmeticTrait.BITWISE in traitsTyped.arithmeticTraits -> ArithmeticTrait.BITWISE + ArithmeticTrait.NONLIN_INT in traitsTyped.arithmeticTraits -> ArithmeticTrait.NONLIN_INT + else -> ArithmeticTrait.LIN_INT + } + + loggerTyped.write(Logger.Level.RESULT, "Using portfolio $mainTrait\n") val inProcess = HierarchicalNode("InProcess", getStm(mainTrait, true)) val notInProcess = HierarchicalNode("NotInprocess", getStm(mainTrait, false)) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt index ab544f379f..306c23ae17 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt @@ -114,6 +114,7 @@ ${edges.map { it.visualize() }.reduce { a, b -> "$a\n$b" }} println("Caught exception: $e") val edge: Edge? = currentNode.outEdges.find { it.trigger(e) } if (edge != null) { + println("Handling exception as ${edge.trigger}") currentNode = edge.target } else { println("Could not handle trigger $e (Available triggers: ${ diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt index a724a1038f..790b810593 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt @@ -53,6 +53,7 @@ fun traceToWitness( for (i in 0 until trace.length()) { val state = trace.states[i] val nextState = trace.states[i + 1] + val newThreads = nextState.processes.keys - state.processes.keys val node = WitnessNode( id = "N${newStates.size}", entry = false, @@ -77,8 +78,11 @@ fun traceToWitness( for (xcfaLabel in flattenedSequence) { val node = WitnessNode(id = "N${newStates.size}", entry = false, sink = false, violation = false) - val edge = labelToEdge(lastNode, node, xcfaLabel, action.pid, + var edge = labelToEdge(lastNode, node, xcfaLabel, action.pid, nextState.sGlobal.getVal(), parseContext) + if (newThreads.isNotEmpty() && xcfaLabel is StartLabel) { + edge = edge.copy(createThread = newThreads.joinToString(",")) + } if (node != WitnessNode(id = "N${newStates.size}") || shouldInclude(edge, verbosity)) { newStates.add(node) newActions.add(edge) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/Witness.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/Witness.kt index 8407379e7a..0b9209b964 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/Witness.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/Witness.kt @@ -71,6 +71,7 @@ class Witness(private val trace: Trace, programFile: F attributes.add( WitnessAttribute("returnFromFunction", "string", "edge", "returnFromFunction")) attributes.add(WitnessAttribute("threadId", "string", "edge", "threadId")) + attributes.add(WitnessAttribute("createThread", "string", "edge", "createThread")) attributes.add(WitnessAttribute("stmt", "string", "edge", "stmt")) attributes.add(WitnessAttribute("cSource", "string", "edge", "cSource")) diff --git a/subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/24return.c b/subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/24return.c new file mode 100644 index 0000000000..7c58083a7b --- /dev/null +++ b/subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/24return.c @@ -0,0 +1,18 @@ +extern int __VERIFIER_nondet_int(); +void reach_error(); + +int b; + +void a() { + int a = __VERIFIER_nondet_int(); + if(a) { + b++; + return; + } + b++; +} + +int main() { + a(); + if(b == 2) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/gson/FrontendMetadataAdapter.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/gson/FrontendMetadataAdapter.kt index 7119455cf2..b829bb2c19 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/gson/FrontendMetadataAdapter.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/gson/FrontendMetadataAdapter.kt @@ -94,44 +94,32 @@ class FrontendMetadataAdapter(val gsonSupplier: () -> Gson) : TypeAdapter() reader.beginArray() - while (reader.hasNext()) { + while (reader.peek() != JsonToken.END_ARRAY) { reader.beginObject() - - var key: String? = null - var value: Any? = null - - while (reader.hasNext()) { - when (reader.nextName()) { - "key" -> { - key = reader.nextString() - } - - "value" -> { - value = readValue(reader) - } - - else -> { - reader.skipValue() - } + if (reader.hasNext()) { + val key = reader.nextName() + val value = readValue(reader) + if (value != null) { + values[key] = value } } reader.endObject() - if (key != null && value != null) { - values[key] = value - } } reader.endArray() return values } - private fun readValue(reader: JsonReader): Any { + private fun readValue(reader: JsonReader): Any? { return when { reader.peek() == JsonToken.STRING -> reader.nextString() reader.peek() == JsonToken.BOOLEAN -> reader.nextBoolean() - else -> reader.skipValue() + else -> { + reader.skipValue() + null + } } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt index 2f1d5c3540..0c8600ddf0 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt @@ -36,7 +36,6 @@ import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType import hu.bme.mit.theta.xcfa.collectVarsWithAccessType import hu.bme.mit.theta.xcfa.isRead import hu.bme.mit.theta.xcfa.model.* -import java.lang.UnsupportedOperationException /** * This pass simplifies the expressions inside statements and substitutes the values of constant variables @@ -71,7 +70,7 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass { CComplexType.getType(it.stmt.cond, parseContext)) } parseContext.metadata.create(simplified, "cTruth", it.stmt.cond is NeqExpr<*>) - StmtLabel(Assume(simplified), metadata = it.metadata) + StmtLabel(Assume(simplified), metadata = it.metadata, choiceType = it.choiceType) } else -> it diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt index 5ae232290c..1f7ce85a16 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt @@ -91,7 +91,9 @@ fun XcfaLabel.changeVars(varLut: Map, VarDecl<*>>, parseContext: Par is StartLabel -> StartLabel(name, params.map { it.changeVars(varLut, parseContext) }, pidVar.changeVars(varLut), metadata = metadata) - is StmtLabel -> StmtLabel(stmt.changeVars(varLut, parseContext), metadata = metadata) + is StmtLabel -> StmtLabel(stmt.changeVars(varLut, parseContext), metadata = metadata, + choiceType = this.choiceType) + is WriteLabel -> WriteLabel(local.changeVars(varLut), global.changeVars(varLut), labels, metadata = metadata) diff --git a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt index aabec68c91..b84e062ca7 100644 --- a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt +++ b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt @@ -26,6 +26,8 @@ import hu.bme.mit.theta.core.type.Type import hu.bme.mit.theta.core.type.inttype.IntExprs.Int import hu.bme.mit.theta.core.utils.indexings.BasicVarIndexing import hu.bme.mit.theta.core.utils.indexings.VarIndexing +import hu.bme.mit.theta.frontend.FrontendMetadata +import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.grammar.dsl.expr.ExpressionWrapper import hu.bme.mit.theta.grammar.dsl.stmt.StatementWrapper import hu.bme.mit.theta.grammar.dsl.type.TypeWrapper @@ -62,6 +64,10 @@ class GsonTest { gsonBuilder.registerTypeHierarchyAdapter(MetaData::class.java, MetaDataAdapter()) gsonBuilder.registerTypeHierarchyAdapter(Pair::class.java, PairAdapter { gson }) gsonBuilder.registerTypeHierarchyAdapter(Optional::class.java, OptionalAdapter { gson }) + gsonBuilder.registerTypeHierarchyAdapter(ParseContext::class.java, + ParseContextAdapter { gson }) + gsonBuilder.registerTypeHierarchyAdapter(FrontendMetadata::class.java, + FrontendMetadataAdapter { gson }) gson = gsonBuilder.create() return gson } @@ -95,4 +101,20 @@ class GsonTest { assertEquals(xcfaSource, output) } + @Test + fun testParseContextRoundTrip() { + val parseContext = ParseContext() + parseContext.metadata.create("owner", "key", "value") + + val symbolTable = XcfaScope(SymbolTable()) + val x_symbol = NamedSymbol("x") + symbolTable.add(x_symbol) + val env = Env() + + val gson = getGson(symbolTable, env, true) + assertEquals(parseContext.metadata.lookupKeyValue, + gson.fromJson(gson.toJson(parseContext), ParseContext::class.java).metadata.lookupKeyValue) + + } + } \ No newline at end of file