Commit 71a888d6 authored by Ludwig Dickmanns's avatar Ludwig Dickmanns
Browse files

MCDC: toZ3 Clean-up

* Removed println
* Removed high level instanceofs
* Added questions for discussion in meeting


Issue-Ref: 3465
Issue-Url: https://af3-developer.fortiss.org/issues/3465

Signed-off-by: Ludwig Dickmanns's avatarLudwig Dickmanns <dickmanns@fortiss.org>
parent cd783f9d
......@@ -27,12 +27,10 @@ import org.fortiss.af3.expression.model.terms.Const;
import org.fortiss.af3.expression.model.terms.DoubleConst;
import org.fortiss.af3.expression.model.terms.EOperator;
import org.fortiss.af3.expression.model.terms.FunctionCall;
import org.fortiss.af3.expression.model.terms.IExpressionTerm;
import org.fortiss.af3.expression.model.terms.IntConst;
import org.fortiss.af3.expression.model.terms.PredefinedFunction;
import org.fortiss.af3.expression.model.terms.Var;
import org.fortiss.af3.expression.model.terms.imperative.Assignment;
import org.fortiss.af3.expression.model.terms.imperative.IStatementTerm;
import org.fortiss.af3.expression.model.types.TBool;
import org.fortiss.af3.expression.model.types.TDouble;
import org.fortiss.af3.expression.model.types.TInt;
......@@ -66,114 +64,97 @@ public final class MCDCUtils {
*/
// TODO(HP): Remove the println
// TODO(HP): Way to many nested ifs. maybe use pattern matching.
// Also, it would be better to just check "instance of X" for the Xs in the lowest level of the type hierarchy (BoolConst, Var, FunctionCall,
// instead of IStatementTerm or IExpressionTerm) and just return null if not of the cases match that.
// Also, it would be better to just check "instance of X" for the Xs in the lowest level of the
// type hierarchy (BoolConst, Var, FunctionCall,
// instead of IStatementTerm or IExpressionTerm) and just return null if not of the cases match
// that.
// Is there a getID function for IDs of the TermsPackage for switch case?? Or aren't the ifs too
// nested?
// The highlevel checks were there to identify the lowest level unmatched case (e.g. unmatched
// IExpressionTerm as print instead of only saying unmatched)
public static Expr toZ3(String prefix, Context ctx, ITerm term, EObject context) {
if(term instanceof IStatementTerm) {
if(term instanceof IExpressionTerm) {
if(term instanceof Const) {
if(term instanceof BoolConst) {
return ctx.mkBool(((BoolConst)term).getValue());
}
if(term instanceof IntConst) {
return ctx.mkInt(((IntConst)term).getValue());
}
if(term instanceof DoubleConst) {
return ctx.mkReal(Double.toString(((DoubleConst)term).getValue()));
}
System.out.println("Unmatched Const: " + term.toString());
return null;
}
if(term instanceof Var) {
// TODO: Carry ifthenelse through recursion to have whole context to search??
// check prefix != 0 -> concat name?
// TODO: just use an empty prefix for the null case?
IType type = getVarType((VarBase)term, context);
if(type instanceof TBool) {
return ctx.mkBoolConst(prefix + ((Var)term).getIdentifier());
}
if(type instanceof TInt) {
return ctx.mkIntConst(prefix + ((Var)term).getIdentifier());
}
if(type instanceof TDouble) {
return ctx.mkRealConst(prefix + ((Var)term).getIdentifier());
}
System.out.println("Unmatched Var: " + ((Var)term).getIdentifier());
return null;
}
if(term instanceof FunctionCall) {
IFunction function = ((FunctionCall)term).getFunction();
if(function instanceof PredefinedFunction) {
PredefinedFunction predefinedFunction = (PredefinedFunction)function;
EOperator operator = predefinedFunction.getOperator();
EList<ITerm> arguments = ((FunctionCall)term).getArguments();
if(arguments.size() == 1) {
// The if clause assures that the list contains exactly one argument.
Expr arg0 = toZ3(prefix, ctx, arguments.get(0), context);
return unaryOperator(ctx, operator, arg0);
}
if(arguments.size() == 2) {
// The if clause assures that the list contains exactly two arguments.
Expr arg0 = toZ3(prefix, ctx, arguments.get(0), context);
Expr arg1 = toZ3(prefix, ctx, arguments.get(1), context);
return binaryOperator(ctx, operator, arg0, arg1);
}
if(arguments.size() > 2) {
return multipleOperator(prefix, ctx, context, operator, arguments);
}
System.out.println("Arguments of PredefinedFunction < 1: " +
term.toString());
// TODO(HP): This is dead code. If the first 2 ifs were false, the 2rd will be true and return.
return null;
}
System.out.println("Unmatched FunctionCall: " + term.toString());
return null;
}
System.out.println("Unmatched IExpressionTerm: " + term.toString());
return null;
if(term instanceof Const) {
if(term instanceof BoolConst) {
return ctx.mkBool(((BoolConst)term).getValue());
}
if(term instanceof Assignment) {
// TODO: Carry ifthenelse through recursion to have whole context to search??
Expr lhs;
Expr rhs = toZ3(prefix, ctx, ((Assignment)term).getValue(), context);
String identifier = ((Assignment)term).getVariable().getIdentifier();
IType type = getVarType(((Assignment)term).getVariable(), context);
if(type instanceof TBool) {
lhs = ctx.mkBoolConst(prefix + identifier);
return ctx.mkEq(lhs, rhs);
}
if(type instanceof TInt) {
lhs = ctx.mkIntConst(prefix + identifier);
return ctx.mkEq(lhs, rhs);
if(term instanceof IntConst) {
return ctx.mkInt(((IntConst)term).getValue());
}
if(term instanceof DoubleConst) {
return ctx.mkReal(Double.toString(((DoubleConst)term).getValue()));
}
return null;
}
if(term instanceof Var) {
// TODO: just use an empty prefix for the null case?
IType type = getVarType((VarBase)term, context);
if(type instanceof TBool) {
return ctx.mkBoolConst(prefix + ((Var)term).getIdentifier());
}
if(type instanceof TInt) {
return ctx.mkIntConst(prefix + ((Var)term).getIdentifier());
}
if(type instanceof TDouble) {
return ctx.mkRealConst(prefix + ((Var)term).getIdentifier());
}
return null;
}
if(term instanceof FunctionCall) {
IFunction function = ((FunctionCall)term).getFunction();
if(function instanceof PredefinedFunction) {
PredefinedFunction predefinedFunction = (PredefinedFunction)function;
EOperator operator = predefinedFunction.getOperator();
EList<ITerm> arguments = ((FunctionCall)term).getArguments();
if(arguments.size() == 1) {
// The if clause assures that the list contains exactly one argument.
Expr arg0 = toZ3(prefix, ctx, arguments.get(0), context);
return unaryOperator(ctx, operator, arg0);
}
if(type instanceof TDouble) {
lhs = ctx.mkRealConst(prefix + identifier);
return ctx.mkEq(lhs, rhs);
if(arguments.size() == 2) {
// The if clause assures that the list contains exactly two arguments.
Expr arg0 = toZ3(prefix, ctx, arguments.get(0), context);
Expr arg1 = toZ3(prefix, ctx, arguments.get(1), context);
return binaryOperator(ctx, operator, arg0, arg1);
}
System.out.println("Unmatched Assignment: " + term.toString());
return null;
return multipleOperator(prefix, ctx, context, operator, arguments);
}
return null;
}
if(term instanceof Assignment) {
Expr lhs;
Expr rhs = toZ3(prefix, ctx, ((Assignment)term).getValue(), context);
String identifier = ((Assignment)term).getVariable().getIdentifier();
IType type = getVarType(((Assignment)term).getVariable(), context);
if(type instanceof TBool) {
lhs = ctx.mkBoolConst(prefix + identifier);
return ctx.mkEq(lhs, rhs);
}
if(type instanceof TInt) {
lhs = ctx.mkIntConst(prefix + identifier);
return ctx.mkEq(lhs, rhs);
}
if(type instanceof TDouble) {
lhs = ctx.mkRealConst(prefix + identifier);
return ctx.mkEq(lhs, rhs);
}
// TODO: uncomment when merged in mcdc-master
// if(term instanceof FormalRequirementMCDC) {
// FormalRequirementMCDC formalRequirementMCDC = (FormalRequirementMCDC)term;
// BoolExpr guard = (BoolExpr)toZ3(prefix, ctx, formalRequirementMCDC.getGuard());
// BoolExpr thenE = ctx.mkTrue();
// BoolExpr elseE = ctx.mkTrue();
// for(IStatementTerm statement : formalRequirementMCDC.getThenBlock().getStatements())
// {
// thenE = ctx.mkAnd(thenE, (BoolExpr)toZ3(prefix, ctx, statement));
// }
// for(IStatementTerm statement : formalRequirementMCDC.getElseBlock().getStatements())
// {
// elseE = ctx.mkAnd(elseE, (BoolExpr)toZ3(prefix, ctx, statement));
// }
// return ctx.mkOr(ctx.mkAnd(guard, thenE), ctx.mkAnd(ctx.mkNot(guard), elseE));
// }
System.out.println("Unmatched IStatementTerm: " + term.toString());
return null;
}
System.out.println("Unmatched ITerm: " + term.toString());
// TODO: uncomment when merged in mcdc-master
// if(term instanceof FormalRequirementMCDC) {
// FormalRequirementMCDC formalRequirementMCDC = (FormalRequirementMCDC)term;
// BoolExpr guard = (BoolExpr)toZ3(prefix, ctx, formalRequirementMCDC.getGuard());
// BoolExpr thenE = ctx.mkTrue();
// BoolExpr elseE = ctx.mkTrue();
// for(IStatementTerm statement : formalRequirementMCDC.getThenBlock().getStatements())
// {
// thenE = ctx.mkAnd(thenE, (BoolExpr)toZ3(prefix, ctx, statement));
// }
// for(IStatementTerm statement : formalRequirementMCDC.getElseBlock().getStatements())
// {
// elseE = ctx.mkAnd(elseE, (BoolExpr)toZ3(prefix, ctx, statement));
// }
// return ctx.mkOr(ctx.mkAnd(guard, thenE), ctx.mkAnd(ctx.mkNot(guard), elseE));
// }
return null;
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment