Skip to content

Commit

Permalink
Merge branch 'xcfa-refactor' into xcfa-refactor-struct-init
Browse files Browse the repository at this point in the history 
# Conflicts:
#	subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
  • Loading branch information
@csanadtelbisz
csanadtelbisz committed Nov 1, 2023
2 parents fd8ab34 + 275ee53 commit 08d4d20
Show file tree
Hide file tree
Showing 21 changed files with 618 additions and 93 deletions.
29 changes: 29 additions & 0 deletions ...rojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredAbstractors.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
*/
package hu.bme.mit.theta.analysis.pred;

import hu.bme.mit.theta.analysis.expr.ExprAction;
import hu.bme.mit.theta.common.container.Containers;
import hu.bme.mit.theta.core.decl.ConstDecl;
import hu.bme.mit.theta.core.decl.Decls;
Expand All @@ -23,6 +24,7 @@
import hu.bme.mit.theta.core.type.LitExpr;
import hu.bme.mit.theta.core.type.booltype.BoolExprs;
import hu.bme.mit.theta.core.type.booltype.BoolType;
import hu.bme.mit.theta.core.utils.ExprUtils;
import hu.bme.mit.theta.core.utils.PathUtils;
import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
import hu.bme.mit.theta.solver.Solver;
Expand Down Expand Up @@ -69,6 +71,15 @@ public interface PredAbstractor {
Collection<PredState> createStatesForExpr(final Expr<BoolType> expr,
final VarIndexing exprIndexing,
final PredPrec prec, final VarIndexing precIndexing);

default Collection<PredState> createStatesForExpr(final Expr<BoolType> expr,
final VarIndexing exprIndexing,
final PredPrec prec,
final VarIndexing precIndexing,
final PredState state,
final ExprAction action) {
return createStatesForExpr(expr, exprIndexing, prec, precIndexing);
}
}

/**
Expand Down Expand Up @@ -225,5 +236,23 @@ public Collection<PredState> createStatesForExpr(final Expr<BoolType> expr,
return Collections.singleton(PredState.of(newStatePreds));
}

@Override
public Collection<PredState> createStatesForExpr(final Expr<BoolType> expr,
final VarIndexing exprIndexing,
final PredPrec prec,
final VarIndexing precIndexing,
final PredState state,
final ExprAction action) {
var actionExpr = action.toExpr();
if (actionExpr.equals(True())) {
var filteredPreds = state.getPreds().stream().filter(p -> {
var vars = ExprUtils.getVars(p);
var indexing = action.nextIndexing();
return vars.stream().allMatch(v -> indexing.get(v) == 0);
}).collect(Collectors.toList());
return Collections.singleton(PredState.of(filteredPreds));
}
return createStatesForExpr(expr, exprIndexing, prec, precIndexing);
}
}
}
2 changes: 1 addition & 1 deletion subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredTransFunc.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ public Collection<? extends PredState> getSuccStates(final PredState state,

final Collection<PredState> succStates = predAbstractor.createStatesForExpr(
And(state.toExpr(), action.toExpr()), VarIndexingFactory.indexing(0), prec,
action.nextIndexing());
action.nextIndexing(), state, action);
return succStates.isEmpty() ? Collections.singleton(PredState.bottom()) : succStates;
}

Expand Down
9 changes: 7 additions & 2 deletions ...ects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/CexMonitor.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,13 @@ import hu.bme.mit.theta.common.exception.NotSolvableException
import hu.bme.mit.theta.common.logging.Logger
import java.lang.RuntimeException


// TODO implement mitigation
/**
* This monitor checks whether a new counterexample is found during the current iteration of CEGAR.
* In most cases, finding the same counterexample again means that refinement is not progressing.
* Warning: With some configurations (e.g. lazy pruning) it is NOT impossible that analysis will
* progress even if in some iterations a new cex is not found, but seems to be rare.
* However, if you think analysis should NOT be stopped by this monitor, disable it and check results.
*/
class CexMonitor<S : State?, A : Action?> constructor(
private val mitigate: Boolean, private val logger: Logger, private val arg: ARG<S, A>
) : Monitor {
Expand Down
11 changes: 10 additions & 1 deletion subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,16 @@ public IntLitExpr pos() {
}

public IntLitExpr div(final IntLitExpr that) {
return IntLitExpr.of(this.value.divide(that.value));
// Semantics:
// 5 div 3 = 1
// 5 div -3 = -1
// -5 div 3 = -2
// -5 div -3 = 2
var result = this.value.divide(that.value);
if (this.value.compareTo(BigInteger.ZERO) < 0 && this.value.mod(that.value.abs()).compareTo(BigInteger.ZERO) != 0) {
result = result.subtract(BigInteger.valueOf(that.value.signum()));
}
return IntLitExpr.of(result);
}

public IntLitExpr mod(final IntLitExpr that) {
Expand Down
13 changes: 13 additions & 0 deletions subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,19 @@ public void testIntToRat() {
}
}

@Test
public void testDiv() {
assertEquals(Int(1), evaluate(Div(Int(5), Int(3))));
assertEquals(Int(-1), evaluate(Div(Int(5), Int(-3))));
assertEquals(Int(-2), evaluate(Div(Int(-5), Int(3))));
assertEquals(Int(2), evaluate(Div(Int(-5), Int(-3))));

assertEquals(Int(2), evaluate(Div(Int(6), Int(3))));
assertEquals(Int(-2), evaluate(Div(Int(6), Int(-3))));
assertEquals(Int(-2), evaluate(Div(Int(-6), Int(3))));
assertEquals(Int(2), evaluate(Div(Int(-6), Int(-3))));
}

@Test
public void testMod() {
assertEquals(Int(2), evaluate(Mod(Int(2), Int(3))));
Expand Down
76 changes: 57 additions & 19 deletions ...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,17 +24,16 @@
import hu.bme.mit.theta.core.type.LitExpr;
import hu.bme.mit.theta.core.type.Type;
import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs;
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.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.booltype.BoolExprs;
import hu.bme.mit.theta.core.type.booltype.BoolType;
import hu.bme.mit.theta.core.type.bvtype.BvAndExpr;
import hu.bme.mit.theta.core.type.bvtype.BvExprs;
import hu.bme.mit.theta.core.type.bvtype.BvOrExpr;
import hu.bme.mit.theta.core.type.bvtype.BvType;
import hu.bme.mit.theta.core.type.bvtype.BvXorExpr;
import hu.bme.mit.theta.core.type.bvtype.*;
import hu.bme.mit.theta.core.type.fptype.FpLitExpr;
import hu.bme.mit.theta.core.type.inttype.IntType;
import hu.bme.mit.theta.core.utils.BvUtils;
import hu.bme.mit.theta.core.utils.FpUtils;
import hu.bme.mit.theta.frontend.ParseContext;
Expand All @@ -43,11 +42,7 @@
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.TypedefVisitor;
import hu.bme.mit.theta.frontend.transformation.grammar.type.TypeVisitor;
import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration;
import hu.bme.mit.theta.frontend.transformation.model.statements.CAssignment;
import hu.bme.mit.theta.frontend.transformation.model.statements.CCall;
import hu.bme.mit.theta.frontend.transformation.model.statements.CCompound;
import hu.bme.mit.theta.frontend.transformation.model.statements.CExpr;
import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement;
import hu.bme.mit.theta.frontend.transformation.model.statements.*;
import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType;
import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CArray;
import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer;
Expand All @@ -56,16 +51,11 @@
import org.kframework.mpfr.BinaryMathContext;

import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Deque;
import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.*;
import java.util.stream.Collectors;

import static com.google.common.base.Preconditions.checkState;
import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq;
import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Ite;
import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*;
import static hu.bme.mit.theta.core.type.fptype.FpExprs.FpType;
import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
import static hu.bme.mit.theta.core.utils.TypeUtils.cast;
Expand Down Expand Up @@ -371,10 +361,18 @@ public Expr<?> visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon
expr = AbstractExprs.Mul(leftExpr, rightExpr);
break;
case "/":
expr = AbstractExprs.Div(leftExpr, rightExpr);
if (leftExpr.getType() instanceof IntType && rightExpr.getType() instanceof IntType) {
expr = createIntDiv(leftExpr, rightExpr);
} else {
expr = AbstractExprs.Div(leftExpr, rightExpr);
}
break;
case "%":
expr = AbstractExprs.Mod(leftExpr, rightExpr);
if (leftExpr.getType() instanceof IntType && rightExpr.getType() instanceof IntType) {
expr = createIntMod(leftExpr, rightExpr);
} else {
expr = AbstractExprs.Mod(leftExpr, rightExpr);
}
break;
default:
throw new IllegalStateException("Unexpected value: " + ctx.signs.get(i).getText());
Expand All @@ -388,6 +386,46 @@ public Expr<?> visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon
return ctx.castExpression(0).accept(this);
}

/**
* Conversion from C (/) semantics to solver (div) semantics.
* @param a dividend
* @param b divisor
* @return expression representing C division semantics with solver operations
*/
private Expr<?> createIntDiv(Expr<?> a, Expr<?> b) {
DivExpr<?> aDivB = Div(a, b);
return Ite(Geq(a, Int(0)), // if (a >= 0)
aDivB, // a div b
// else
Ite(Neq(Mod(a, b), Int(0)), // if (a mod b != 0)
Ite(Geq(b, Int(0)), // if (b >= 0)
Add(aDivB, Int(1)), // a div b + 1
// else
Sub(aDivB, Int(1)) // a div b - 1
), // else
aDivB // a div b
)
);
}

/**
* Conversion from C (%) semantics to solver (mod) semantics.
* @param a dividend
* @param b divisor
* @return expression representing C modulo semantics with solver operations
*/
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
)
);
}

@Override
public Expr<?> visitCastExpressionUnaryExpression(CParser.CastExpressionUnaryExpressionContext ctx) {
return ctx.unaryExpression().accept(this);
Expand Down
8 changes: 7 additions & 1 deletion subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
import hu.bme.mit.theta.core.utils.TypeUtils
import hu.bme.mit.theta.solver.Solver
import hu.bme.mit.theta.xcfa.analysis.XcfaProcessState.Companion.createLookup
import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence
import hu.bme.mit.theta.xcfa.getFlatLabels
import hu.bme.mit.theta.xcfa.getGlobalVars
import hu.bme.mit.theta.xcfa.isWritten
Expand All @@ -50,9 +51,14 @@ import java.util.function.Predicate
open class XcfaAnalysis<S : ExprState, P : Prec>(
private val corePartialOrd: PartialOrd<XcfaState<S>>,
private val coreInitFunc: InitFunc<XcfaState<S>, XcfaPrec<P>>,
private val coreTransFunc: TransFunc<XcfaState<S>, XcfaAction, XcfaPrec<P>>,
private var coreTransFunc: TransFunc<XcfaState<S>, XcfaAction, XcfaPrec<P>>,
) : Analysis<XcfaState<S>, XcfaAction, XcfaPrec<P>> {

init {
ConeOfInfluence.coreTransFunc = transFunc as TransFunc<XcfaState<out ExprState>, XcfaAction, XcfaPrec<out Prec>>
coreTransFunc = ConeOfInfluence.transFunc as TransFunc<XcfaState<S>, XcfaAction, XcfaPrec<P>>
}

override fun getPartialOrd(): PartialOrd<XcfaState<S>> = corePartialOrd
override fun getInitFunc(): InitFunc<XcfaState<S>, XcfaPrec<P>> = coreInitFunc
override fun getTransFunc(): TransFunc<XcfaState<S>, XcfaAction, XcfaPrec<P>> = coreTransFunc
Expand Down
Loading

0 comments on commit 08d4d20

Please sign in to comment.