Commit f2d9d559 authored by Hernan Ponce de Leon's avatar Hernan Ponce de Leon
Browse files

Merge branch '3465-IStatementTerm_toZ3' into '3477-MCDC_implementation'

3465 i statement term to z3

See merge request !59
parents a70d7a6d e9a2765d
MCDCUtils.java 7ac114cd2a668169becb4ee2f4568d7b86607478 GREEN
/*-------------------------------------------------------------------------+
| Copyright 2018 fortiss GmbH |
| |
| 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 org.fortiss.af3.testing.mcdc;
import static org.fortiss.af3.project.utils.VariableScopeUtils.getVarType;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.Collectors;
import org.eclipse.emf.common.util.EList;
import org.eclipse.emf.common.util.TreeIterator;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.util.EcoreUtil;
import org.fortiss.af3.expression.model.terms.BoolConst;
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.types.TBool;
import org.fortiss.af3.expression.model.types.TDouble;
import org.fortiss.af3.expression.model.types.TInt;
import org.fortiss.af3.project.model.typesystem.IFunction;
import org.fortiss.af3.project.model.typesystem.ITerm;
import org.fortiss.af3.project.model.typesystem.IType;
import org.fortiss.af3.project.model.typesystem.VarBase;
import org.fortiss.af3.testing.model.mcdc.FormalRequirementMCDC;
import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
import com.microsoft.z3.IntExpr;
import com.microsoft.z3.Z3Exception;
/**
* Utility class transforming a {@link FormalRequirementMCDC} into an {@link Expr}.
*
* @author ludwig dickmanns
*/
public final class MCDCUtils {
/**
* Transforms a {@link ITerm} into a {@link Expr}.
*
* @param prefix
* @param ctx
* @param term
* @param context
* @return the {@link Expr} for an {@link ITerm} or <code>null</code> for invalid inputs.
*/
public static Expr toZ3(String prefix, Context ctx, ITerm term, EObject context) {
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()));
}
if(term instanceof Var) {
IType type = getVarType((VarBase)term, context);
String identifier = ((Var)term).getIdentifier();
if(type instanceof TBool) {
return ctx.mkBoolConst(prefix + identifier);
}
if(type instanceof TInt) {
return ctx.mkIntConst(prefix + identifier);
}
if(type instanceof TDouble) {
return ctx.mkRealConst(prefix + identifier);
}
}
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() == 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);
}
return multipleOperator(prefix, ctx, context, operator, arguments);
}
}
if(term instanceof Assignment) {
Expr lhs = null;
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);
}
if(type instanceof TInt) {
lhs = ctx.mkIntConst(prefix + identifier);
}
if(type instanceof TDouble) {
lhs = ctx.mkRealConst(prefix + identifier);
}
if(lhs != null) {
return ctx.mkEq(lhs, rhs);
}
return null;
}
return null;
}
/** Binary Operators of {@link PredefinedFunction}. */
private static Expr binaryOperator(Context ctx, EOperator operator, Expr arg0, Expr arg1) {
try {
switch(operator) {
case ADD:
return ctx.mkAdd((ArithExpr)arg0, (ArithExpr)arg1);
case SUBTRACT:
return ctx.mkSub((ArithExpr)arg0, (ArithExpr)arg1);
case MULTIPLY:
return ctx.mkMul((ArithExpr)arg0, (ArithExpr)arg1);
case DIVIDE:
return ctx.mkDiv((ArithExpr)arg0, (ArithExpr)arg1);
case MODULO:
return ctx.mkMod((IntExpr)arg0, (IntExpr)arg1);
case LOWER_THAN:
return ctx.mkLt((ArithExpr)arg0, (ArithExpr)arg1);
case GREATER_THAN:
return ctx.mkGt((ArithExpr)arg0, (ArithExpr)arg1);
case LOWER_EQUAL:
return ctx.mkLe((ArithExpr)arg0, (ArithExpr)arg1);
case GREATER_EQUAL:
return ctx.mkGe((ArithExpr)arg0, (ArithExpr)arg1);
case EQUAL:
return ctx.mkEq(arg0, arg1);
case NOT_EQUAL:
return ctx.mkNot(ctx.mkEq(arg0, arg1));
case OR:
return ctx.mkOr((BoolExpr)arg0, (BoolExpr)arg1);
case AND:
return ctx.mkAnd((BoolExpr)arg0, (BoolExpr)arg1);
default:
return null;
}
} catch(Z3Exception e) {
System.out.println(e.toString());
return null;
}
}
/** Operator with multiple arguments of {@link PredefinedFunction}. */
private static Expr multipleOperator(String prefix, Context ctx, EObject context,
EOperator operator, EList<ITerm> args) {
try {
if(operator == EOperator.ADD || operator == EOperator.SUBTRACT ||
operator == EOperator.MULTIPLY) {
List<ArithExpr> tmp =
args.stream().map(e -> (ArithExpr)toZ3(prefix, ctx, e, context))
.collect(Collectors.toList());
switch(operator) {
case ADD:
return ctx.mkAdd(tmp.toArray(new ArithExpr[tmp.size()]));
case SUBTRACT:
return ctx.mkSub(tmp.toArray(new ArithExpr[tmp.size()]));
case MULTIPLY:
return ctx.mkMul(tmp.toArray(new ArithExpr[tmp.size()]));
}
}
if(operator == EOperator.OR || operator == EOperator.AND) {
List<BoolExpr> tmp =
args.stream().map(e -> (BoolExpr)toZ3(prefix, ctx, e, context))
.collect(Collectors.toList());
switch(operator) {
case OR:
return ctx.mkOr(tmp.toArray(new BoolExpr[tmp.size()]));
case AND:
return ctx.mkAnd(tmp.toArray(new BoolExpr[tmp.size()]));
}
}
return null;
} catch(Z3Exception e) {
System.out.println(e.toString());
return null;
}
}
/**
* @param guard
* - the guard from which the atoms should be extracted.
* @return a list of Atoms, which are a equation or inequation only containing a single argument
* on both sides (either a {@link Var} or a {@link Const}).
*/
public static List<FunctionCall> getAtomsFromGuardMCDC(IExpressionTerm guard) {
List<FunctionCall> atoms = new ArrayList<FunctionCall>();
if(isAtom(guard)) {
// Wild cast works: see isAtom(guard).
atoms.add((FunctionCall)guard);
return atoms;
}
TreeIterator<EObject> iterator = EcoreUtil.getAllContents(guard, true);
while(iterator.hasNext()) {
EObject eObject = iterator.next();
if(isAtom(eObject)) {
// Wild cast works: see isAtom(guard).
atoms.add((FunctionCall)eObject);
}
}
return atoms;
}
/** Helper method checking whether the object is an atom. */
private static boolean isAtom(EObject eObject) {
if(eObject instanceof FunctionCall) {
FunctionCall functionCall = (FunctionCall)eObject;
IFunction function = functionCall.getFunction();
if(function instanceof PredefinedFunction && functionCall.getArguments().size() == 2) {
PredefinedFunction predefinedFunction = (PredefinedFunction)function;
EOperator operator = predefinedFunction.getOperator();
switch(operator) {
case LOWER_THAN:
case GREATER_THAN:
case LOWER_EQUAL:
case GREATER_EQUAL:
case EQUAL:
case NOT_EQUAL:
// The condition above ensures that there are exactly two arguments
ITerm lhs = functionCall.getArguments().get(0);
ITerm rhs = functionCall.getArguments().get(1);
boolean isLhsCorrect = lhs instanceof Const || lhs instanceof Var;
boolean isRhsCorrect = rhs instanceof Const || rhs instanceof Var;
if(isLhsCorrect && isRhsCorrect) {
return true;
}
break;
default:
break;
}
}
}
return false;
}
}
/*-------------------------------------------------------------------------+
| Copyright 2018 fortiss GmbH |
| |
| 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 test.org.fortiss.af3.testing.mcdc;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.and;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.createVar;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.greaterThan;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.intConst;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.lowerThan;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.or;
import static org.fortiss.af3.testing.mcdc.MCDCUtils.getAtomsFromGuardMCDC;
import org.fortiss.af3.expression.model.terms.FunctionCall;
import org.fortiss.af3.expression.model.terms.IExpressionTerm;
import org.fortiss.af3.expression.model.terms.Var;
import org.fortiss.af3.expression.utils.ExpressionModelElementFactory;
import org.junit.Test;
/**
*
* @author ludwig
*/
public class TestGetAtomsFromGuardMCDC {
@Test
public void test() {
IExpressionTerm guard, a, b;
Var v1 = createVar("v1");
Var v2 = createVar("v2");
a = lowerThan(v1, intConst(42));
b = or(greaterThan(v2, intConst(42)), ExpressionModelElementFactory.equal(v1, v2));
guard = and(a, b);
System.out.println(guard);
System.out.println();
System.out.println("Guard");
for(FunctionCall functionCall : getAtomsFromGuardMCDC(guard)) {
System.out.println(functionCall);
}
System.out.println();
System.out.println("a");
for(FunctionCall functionCall : getAtomsFromGuardMCDC(a)) {
System.out.println(functionCall);
}
System.out.println();
System.out.println("b");
for(FunctionCall functionCall : getAtomsFromGuardMCDC(b)) {
System.out.println(functionCall);
}
}
}
/*-------------------------------------------------------------------------+
| Copyright 2018 fortiss GmbH |
| |
| 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 test.org.fortiss.af3.testing.mcdc;
import static org.fortiss.af3.component.utils.ComponentModelElementFactory.createComponent;
import static org.fortiss.af3.component.utils.ComponentModelElementFactory.createInputPortAndAttach;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.add;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.and;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.assignment;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.boolConst;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.boolType;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.createNoVal;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.divide;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.doubleConst;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.doubleType;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.equal;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.greaterEqual;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.greaterThan;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.intConst;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.intType;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.lowerEqual;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.lowerThan;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.modulo;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.multiply;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.not;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.notEqual;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.or;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.subtract;
import java.util.ArrayList;
import java.util.List;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.component.model.Port;
import org.fortiss.af3.expression.model.terms.BoolConst;
import org.fortiss.af3.expression.model.terms.Const;
import org.fortiss.af3.expression.model.terms.DoubleConst;
import org.fortiss.af3.expression.model.terms.IExpressionTerm;
import org.fortiss.af3.expression.model.terms.IntConst;
import org.fortiss.af3.expression.model.terms.Var;
import org.fortiss.af3.expression.model.terms.imperative.IStatementTerm;
import org.fortiss.af3.project.model.typesystem.IType;
import org.fortiss.af3.testing.mcdc.MCDCUtils;
import org.junit.Test;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
/**
*
* @author ludwig
*/
public class TestMCDCUtils {
private Context ctx = null;
private Component component = null;
/**
* Test case for transformation of the following {@link Const}s to z3 {@link Expr}s:
*
* BoolConst, IntConst, DoubleConst.
*/
@Test
public void test00() {
String description = "Transformation of Consts";
init(0, description);
BoolConst bc0 = boolConst(false);
BoolConst bc1 = boolConst(true);
IntConst ic0 = intConst(-42);
IntConst ic1 = intConst(0);
IntConst ic2 = intConst(42);
DoubleConst dc0 = doubleConst(-4.2);
DoubleConst dc1 = doubleConst(-42);
DoubleConst dc2 = doubleConst(0);
DoubleConst dc3 = doubleConst(0.0);
DoubleConst dc4 = doubleConst(42);
DoubleConst dc5 = doubleConst(2.4);
List<IStatementTerm> list =
listWithMultipleArgs(bc0, bc1, ic0, ic1, ic2, dc0, dc1, dc2, dc3, dc4, dc5);
summary(list);
}
/**
* Test case for transformation of the following {@link IType} {@link Var}s to z3 {@link Expr}s:
*
* TBool, TInt, TDouble.
*/
@Test
public void test01() {
String description = "Transformation of Vars";
init(1, description);
// Ports.
Port b0Port = createInputPortAndAttach(component, "b0", boolType(), createNoVal());
Port i0Port = createInputPortAndAttach(component, "i0", intType(), createNoVal());
Port d0Port = createInputPortAndAttach(component, "d0", doubleType(), createNoVal());
// Vars.
Var b0 = b0Port.getVar();
Var i0 = i0Port.getVar();
Var d0 = d0Port.getVar();
List<IStatementTerm> list = listWithMultipleArgs(b0, i0, d0);
summary(list);
}
/** Test case for unary operator not. */
@Test
public void test02() {
String description = "Transformation of unary operator not";
init(2, description);
// Ports.
Port b0Port = createInputPortAndAttach(component, "b0", boolType(), createNoVal());
// Vars.
Var b0 = b0Port.getVar();
IExpressionTerm not = not(b0);
List<IStatementTerm> list = listWithMultipleArgs(not);
summary(list);
}
/**
* Test case for binary operators.
*
* ADD, SUBSTRACT, MULTIPLY, DIVIDE, MODULO, LOWER_THAN, LOWER_EQUAL, EQUAL, GREATER_EQUAL,
* GREATER_THAN, NOT_EQUAL, OR, AND.
*/
@Test
public void test03() {
String description = "Transformation of binary operators";
init(3, description);
// Ports.
Port b0Port = createInputPortAndAttach(component, "b0", boolType(), createNoVal());
Port i0Port = createInputPortAndAttach(component, "i0", intType(), createNoVal());
Port d0Port = createInputPortAndAttach(component, "d0", doubleType(), createNoVal());
// Vars.
Var b0 = b0Port.getVar();
Var i0 = i0Port.getVar();
Var d0 = d0Port.getVar();
IExpressionTerm add = add(i0, intConst(42));
IExpressionTerm sub = subtract(doubleConst(42.0), d0);
IExpressionTerm mul = multiply(doubleConst(1.0), doubleConst(3.0));
IExpressionTerm div = divide(doubleConst(0.0), doubleConst(4.0));
IExpressionTerm mod = modulo(intConst(23), intConst(4));
IExpressionTerm lt = lowerThan(intConst(0), intConst(4));
IExpressionTerm le = lowerEqual(intConst(0), intConst(4));
IExpressionTerm eq = equal(intConst(0), intConst(4));
IExpressionTerm ge = greaterEqual(intConst(0), intConst(4));
IExpressionTerm gt = greaterThan(intConst(0), intConst(4));
IExpressionTerm ne = notEqual(intConst(0), intConst(4));
IExpressionTerm or = or(b0, boolConst(false));
IExpressionTerm and = and(boolConst(true), b0);
List<IStatementTerm> list =
listWithMultipleArgs(add, sub, mul, div, mod, lt, le, eq, ge, gt, ne, or, and);
summary(list);
}
/**
* Test case for operators with multiple arguments.
*
* ADD, MULTIPLY, OR, AND.
*/
@Test
public void test04() {
String description = "Transformation of operators with multiple arguments";
init(4, description);
// Ports.
Port b0Port = createInputPortAndAttach(component, "b0", boolType(), createNoVal());
Port b1Port = createInputPortAndAttach(component, "b1", boolType(), createNoVal());
Port b2Port = createInputPortAndAttach(component, "b2", boolType(), createNoVal());
Port i0Port = createInputPortAndAttach(component, "i0", intType(), createNoVal());
Port i1Port = createInputPortAndAttach(component, "i1", intType(), createNoVal());
Port i2Port = createInputPortAndAttach(component, "i2", intType(), createNoVal());
Port d0Port = createInputPortAndAttach(component, "d0", doubleType(), createNoVal());
Port d1Port = createInputPortAndAttach(component, "d1", doubleType(), createNoVal());
Port d2Port = createInputPortAndAttach(component, "d2", doubleType(), createNoVal());
// Vars.
Var b0 = b0Port.getVar();
Var b1 = b1Port.getVar();
Var b2 = b2Port.getVar();
Var i0 = i0Port.getVar();
Var i1 = i1Port.getVar();
Var i2 = i2Port.getVar();
Var d0 = d0Port.getVar();
Var d1 = d1Port.getVar();
Var d2 = d2Port.getVar();
List<IExpressionTerm> args;
args = listWithMultipleArgs(i0, i1, i2, intConst(22));
IExpressionTerm add0 = add(args);
args = listWithMultipleArgs(d0, d1, d2, doubleConst(2.0));
IExpressionTerm add1 = add(args);
args = listWithMultipleArgs(b0, b1, b2, boolConst(false));
IExpressionTerm or = or(args);
args = listWithMultipleArgs(b0, b1, b2, boolConst(true));
IExpressionTerm and = and(args);
List<IStatementTerm> list = listWithMultipleArgs(add0, add1, or, and);