LoopContractTransformerWorker.java
package dev.civl.mc.transform.common;
import java.util.Arrays;
import java.util.LinkedList;
import java.util.List;
import dev.civl.abc.ast.IF.AST;
import dev.civl.abc.ast.IF.ASTFactory;
import dev.civl.abc.ast.node.IF.ASTNode;
import dev.civl.abc.ast.node.IF.ASTNode.NodeKind;
import dev.civl.abc.ast.node.IF.NodeFactory;
import dev.civl.abc.ast.node.IF.SequenceNode;
import dev.civl.abc.ast.node.IF.declaration.FunctionDefinitionNode;
import dev.civl.abc.ast.node.IF.declaration.VariableDeclarationNode;
import dev.civl.abc.ast.node.IF.expression.ExpressionNode;
import dev.civl.abc.ast.node.IF.expression.FunctionCallNode;
import dev.civl.abc.ast.node.IF.expression.OperatorNode.Operator;
import dev.civl.abc.ast.node.IF.expression.StringLiteralNode;
import dev.civl.abc.ast.node.IF.statement.BlockItemNode;
import dev.civl.abc.ast.node.IF.statement.DeclarationListNode;
import dev.civl.abc.ast.node.IF.statement.ForLoopInitializerNode;
import dev.civl.abc.ast.node.IF.statement.ForLoopNode;
import dev.civl.abc.ast.node.IF.statement.LoopNode;
import dev.civl.abc.ast.node.IF.statement.LoopNode.LoopKind;
import dev.civl.abc.ast.node.IF.statement.StatementNode;
import dev.civl.abc.ast.node.IF.statement.StatementNode.StatementKind;
import dev.civl.abc.front.IF.CivlcTokenConstant;
import dev.civl.abc.token.IF.CivlcToken;
import dev.civl.abc.token.IF.CivlcToken.TokenVocabulary;
import dev.civl.abc.token.IF.Formation;
import dev.civl.abc.token.IF.Source;
import dev.civl.abc.token.IF.StringLiteral;
import dev.civl.abc.token.IF.SyntaxException;
public class LoopContractTransformerWorker extends BaseWorker {
/**
* A reference to {@link NodeFactory}
*/
private NodeFactory nodeFactory;
/* ************************ Static fields ****************************** */
/* *** Function identifiers *** */
private final static String ASSUME_PUSH = "$assume_push";
private final static String ASSUME_POP = "$assume_pop";
private final static String WRITE_SET_PUSH = "$write_set_push";
private final static String WRITE_SET_POP = "$write_set_pop";
private final static String MEM_EMPTY = "$mem_empty";
private final static String MEM_CONTAINS = "$mem_contains";
private final static String MEM_UNION = "$mem_union";
private final static String MEM_UNION_WIDENING = "$mem_union_widening";
private final static String MEM_UNARY_WIDENING = "$mem_unary_widening";
private final static String MEM_HAVOC = "$mem_havoc";
@Deprecated
private final static String MEM_HAVOC_SIDECOND = "$mem_havoc_sidecond";
// private final static String MEM_ASSIGN_FROM = "$mem_assign_from";
//
// private final static String GET_FULL_STATE = "$get_full_state";
/* *** Generated identifier prefixes: *** */
/**
* Names for miscellaneous temporary variables that do not need to be passed
* among different methods.
*/
private final static String LOOP_TMP_VAR_PREFIX = "_loop_tmp";
/* *** counters for generating unique identifiers *** */
private int loopTmpCounter = 0;
/* ************** primitives for error reporting **************** */
/**
* The token used to construct a {@link StringLiteral} which is used to
* report assertion violation.
*/
private final CivlcToken loopInvariantsViolationMessageToken;
/**
* The static string literal of loop invariants violation messages
*/
private static final String violationMessage = "\"loop invariants violation\"";
/**
* The token used to construct a {@link StringLiteral} which is used to
* report frame condition violation.
*/
private final CivlcToken frameConditionViolationMessageToken;
/**
* The static string literal of frame condition violation messages
*/
private static final String frameConditionViolationMessage = "\"loop assigns violation\"";
/**
* The token used to construct a {@link StringLiteral} which is used to
* report assertion establish violation.
*/
private final CivlcToken loopInvariantsEstablishViolationMessageToken;
/**
* The static string literal of loop invariants establish violation messages
*/
private static final String establishViolationMessage = "\"loop invariants establish violation\"";
/* ******************** static methods ********************** */
/**
* @param node
* An {@link ASTNode}.
* @return true iff the given {@link ASTNode} represents a function
* definition.
*/
static private boolean isFunctionDefinition(ASTNode node) {
return node.nodeKind() == NodeKind.FUNCTION_DEFINITION;
}
/**
* @param node
* An {@link ASTNode}.
* @return true iff the given {@link ASTNode} represents a loop.
*/
static private boolean isLoopNode(ASTNode node) {
if (node.nodeKind() == NodeKind.STATEMENT)
return ((StatementNode) node).statementKind() == StatementKind.LOOP;
return false;
}
/**
* @param node
* An {@link LoopNode}.
* @return true iff the given {@link LoopNode} represents a loop.
*/
static private boolean isContractedLoop(LoopNode loop) {
return loop.loopContracts() != null
&& loop.loopContracts().numChildren() > 0;
}
/**
* @param loop
* An {@link LoopNode}.
* @return true iff the given {@link LoopNode} represents a for-loop.
*/
static private boolean isForLoop(LoopNode loop) {
return loop.getKind() == LoopKind.FOR;
}
/* ******************* Constructor ********************** */
/**
* @return A unique identifier name for miscellaneous variables which are
* only used by within one Java method.
*/
private String nextLoopTmpIdentifier() {
return LOOP_TMP_VAR_PREFIX + loopTmpCounter++;
}
/* ******************* Constructor ********************** */
public LoopContractTransformerWorker(String transformerName,
ASTFactory astFactory) throws SyntaxException {
super(transformerName, astFactory);
this.nodeFactory = astFactory.getNodeFactory();
Formation feedBackformation = tokenFactory
.newTransformFormation(transformerName, "violation report");
frameConditionViolationMessageToken = tokenFactory.newCivlcToken(
CivlcTokenConstant.STRING_LITERAL,
frameConditionViolationMessage, feedBackformation,
TokenVocabulary.DUMMY);
loopInvariantsViolationMessageToken = tokenFactory.newCivlcToken(
CivlcTokenConstant.STRING_LITERAL, violationMessage,
feedBackformation, TokenVocabulary.DUMMY);
loopInvariantsEstablishViolationMessageToken = tokenFactory
.newCivlcToken(CivlcTokenConstant.STRING_LITERAL,
establishViolationMessage, feedBackformation,
TokenVocabulary.DUMMY);
}
/* **************** Main transformation logic methods ****************** */
@Override
protected AST transformCore(AST ast) throws SyntaxException {
SequenceNode<BlockItemNode> root = ast.getRootNode();
boolean hasContractedLoop = false;
ast.release();
for (BlockItemNode block : root) {
if (isFunctionDefinition(block)) {
FunctionDefinitionNode funcDefi = (FunctionDefinitionNode) block;
if (transformLoopInFunction(funcDefi.getBody()))
hasContractedLoop = true;
}
}
if (!hasContractedLoop)
return astFactory.newAST(root, ast.getSourceFiles(),
ast.isWholeProgram());;
ast = astFactory.newAST(root, ast.getSourceFiles(),
ast.isWholeProgram());
// ast.prettyPrint(System.out, true);
return ast;
}
/**
* Given a function body, transform all contracted loops in it into CIVL-C
* codes.
*
* @param body
* The root node of a sub-ASTree representing a function body
* @return true iff at least one loop in this function has been annotated
* @throws SyntaxException
*/
private boolean transformLoopInFunction(BlockItemNode body)
throws SyntaxException {
ASTNode node = body;
LoopContractBlock annotatedLoop;
ASTNode parent = body.parent();
int bodyChildIdx = body.childIndex();
boolean hasContractedLoop = false;
// temporarily take off the body so that the DFS will only traverse the
// body:
body.remove();
do {
// transform nested function definitions:
if (isFunctionDefinition(node)) {
boolean innerHasContractedLoop = transformLoopInFunction(
((FunctionDefinitionNode) node).getBody());
if (innerHasContractedLoop)
hasContractedLoop = true;
}
// transform loop:
if (isLoopNode(node)) {
LoopNode loop = (LoopNode) node;
if (isContractedLoop(loop)) {
// transform the loop
annotatedLoop = new LoopContractBlock(loop);
// skip the whole loop then continue. The loopNode will be
// removed in transformLoopWorker method, so the Skip call
// must happen before it.
node = BaseWorker.nextDFSSkip(loop);
transformLoopWorker(annotatedLoop);
hasContractedLoop = true;
continue;
}
}
node = node.nextDFS();
} while (node != null);
parent.setChild(bodyChildIdx, body);
return hasContractedLoop;
}
/**
* Transform a contracted loop including nested ones into pure CIVL-C codes.
*
* @param loop
* @throws SyntaxException
*/
private void transformLoopWorker(LoopContractBlock loop)
throws SyntaxException {
// transform inner loops
transformLoopInFunction(loop.getLoopNode().getBody());
List<BlockItemNode> LISEComponents = new LinkedList<>();
ASTNode loopParent = loop.getLoopNode().parent();
int childIdx = loop.getLoopNode().childIndex();
if (!loop.getLoopAssignSet().isEmpty()) {
// transforms loop body with [loop-assigns]:
LISEComponents
.add(toNDBranch(loop, inductionStepWithAssigns(loop)));
} else {
// transforms loop body by inferring [loop-assigns] automatically:
String writeSetName = nextLoopTmpIdentifier();
LISEComponents.add(memTypeVariableDeclaration(writeSetName));
LISEComponents
.addAll(inductionStepInferringAssigns(loop, writeSetName));
LISEComponents.addAll(createConclusion(loop, writeSetName));
}
Source source = loop.getLoopNode().getSource();
BlockItemNode LISEBlock = nodeFactory.newCompoundStatementNode(source,
LISEComponents);
loop.getLoopNode().remove();
loopParent.setChild(childIdx, LISEBlock);
}
/* **************** Loop transformation helper methods ****************** */
/**
* <p>
* Transform the loop body to the form that proves the induction step w.r.t
* the given invariants through computing the write set until a fixed-point
* reached.
* </p>
*
* <code>
* $mem ws = $mem_empty();
* $assert(loop-inv); // base case establishment
* while ($choose_int(1)) {
* $mem_havoc(ws);
* $assume_push([loop-inv] && [loop-cond]);
* $write_push();
* [loop-body]
* $assert([loop-inv]); // invariant preserves
*
* $mem tmp = $write_pop();
*
* ws = $mem_union_widening(ws, tmp);
* $assume_pop();
* }
* </code>
*/
private List<BlockItemNode> inductionStepInferringAssigns(
LoopContractBlock loop, String collectedWriteSetName)
throws SyntaxException {
List<BlockItemNode> result = new LinkedList<>();
result.addAll(getForLoopInitializers(loop));
result.add(createAssertion(loop.getLoopInvariants(nodeFactory), 0));
result.add(createAssignment(identifierExpression(collectedWriteSetName),
createMemEmptyCall()));
List<BlockItemNode> whileLoopBody = new LinkedList<>();
ExpressionNode inv = loop.getLoopInvariants(nodeFactory);
ExpressionNode loopCond = loop.getLoopNode().getCondition();
Source invAndCondSource = tokenFactory.join(inv.getSource(),
loopCond.getSource());
ExpressionNode invAndCond = nodeFactory.newOperatorNode(
invAndCondSource, Operator.LAND, inv.copy(), loopCond.copy());
whileLoopBody.addAll(createMemHavoc(collectedWriteSetName));
whileLoopBody.add(createAssumptionPush(invAndCond));
whileLoopBody.add(createWriteSetPush());
whileLoopBody.add(wrapLoopBody(loop));
// assert (inv);
whileLoopBody.add(createAssertion(inv.copy(), 2));
String tmpWsName = nextLoopTmpIdentifier();
whileLoopBody.add(memTypeVariableDeclaration(tmpWsName));
// pop write set
whileLoopBody.add(createWriteSetPop(tmpWsName));
whileLoopBody.add(createMemUnionWidening(collectedWriteSetName,
tmpWsName, collectedWriteSetName));
whileLoopBody.add(createAssumptionPop());
ExpressionNode choiceAsCond = createNDBinaryChoice();
Source whileLoopSource = joinSource(whileLoopBody);
result.add(nodeFactory.newWhileLoopNode(whileLoopSource, choiceAsCond,
nodeFactory.newCompoundStatementNode(whileLoopSource,
whileLoopBody),
null));
return result;
}
/**
* <p>
* the induction proof code for a loop body.
* </p>
*
* <p>
* The translation is : <code>
* $assert(loop-inv); // base case establishment
*
* $mem ws = $mem_union([loop-assigns]);
*
* $mem_havoc(ws);
* $assume([loop-inv] && [loop-cond]);
* $write_set_push();
* [loop-body];
*
* $mem tmp = $write_set_pop();
*
* $assert($mem_contains(ws, tmp));
* $assert([loop-inv]);
* while(true); // to an endless loop so that this state space path ends
* </code>
* </p>
*
* @throws SyntaxException
*/
private List<BlockItemNode> inductionStepWithAssigns(LoopContractBlock loop)
throws SyntaxException {
assert !loop.getLoopAssignSet().isEmpty();
List<BlockItemNode> results = new LinkedList<>();
ExpressionNode inv = loop.getLoopInvariants(nodeFactory);
ExpressionNode loopCond = loop.getLoopNode().getCondition();
Source invAndCondSource = tokenFactory.join(inv.getSource(),
loopCond.getSource());
ExpressionNode invAndCond = nodeFactory.newOperatorNode(
invAndCondSource, Operator.LAND, inv.copy(), loopCond.copy());
String writeSetName = nextLoopTmpIdentifier();
results.addAll(getForLoopInitializers(loop));
results.add(createAssertion(loop.getLoopInvariants(nodeFactory), 0));
// declaring a $mem variable for holding the set of modified memory
// locations:
results.add(memTypeVariableDeclaration(writeSetName));
// havoc the change set either specified in loop assigns:
results.addAll(unionLoopAssigns(loop.getLoopAssignSet(), writeSetName));
results.addAll(createMemHavoc(writeSetName));
// assume([loop-inv] && [loop-cond]) ...
results.add(assumeNode(invAndCond));
// write set push ...
results.add(createWriteSetPush());
// original body ...
results.add(wrapLoopBody(loop));
// assert (inv);
results.add(createAssertion(inv.copy(), 2));
String tmpWsName = nextLoopTmpIdentifier();
results.add(memTypeVariableDeclaration(tmpWsName));
// pop write set:
results.add(createWriteSetPop(tmpWsName));
// check frame-condition:
results.addAll(checkFrameCondition(tmpWsName, writeSetName));
// add endless loop to terminate the search path:
results.addAll(endlessWhileLoop());
return results;
}
/**
* Wraps the original loop body (and the incrementor if it is a for-loop) in
* a pair of curly-braces.
*/
private BlockItemNode wrapLoopBody(LoopContractBlock loop) {
// original body ...
List<BlockItemNode> bodyAndIncrementor = new LinkedList<>();
StatementNode originalBody = loop.getLoopNode().getBody();
bodyAndIncrementor.add(originalBody);
originalBody.remove();
// for-loop incrementer ...
bodyAndIncrementor.addAll(getForLoopIncrementors(loop));
// wrap the original body with a pair of curly braces so that loop-body
// local variables won't be saved in the write set:
return nodeFactory.newCompoundStatementNode(originalBody.getSource(),
bodyAndIncrementor);
}
/**
*
* @return the loop initializers of the <code>loop</code>, if it is a
* for-loop; empty list otherwise.
*/
private List<BlockItemNode> getForLoopInitializers(LoopContractBlock loop) {
List<BlockItemNode> result = new LinkedList<>();
// loop initializer:
if (isForLoop(loop.getLoopNode())) {
ForLoopNode forLoop = (ForLoopNode) loop.getLoopNode();
ForLoopInitializerNode initializer = forLoop.getInitializer();
if (initializer != null) {
if (initializer instanceof ExpressionNode)
result.add(nodeFactory.newExpressionStatementNode(
(ExpressionNode) initializer.copy()));
else {
DeclarationListNode declList = (DeclarationListNode) initializer;
for (VariableDeclarationNode decl : declList) {
result.add(decl.copy());
}
}
}
}
return result;
}
/**
* @returns copy of loop incrementors of the <code>loop</code> if it is a
* for-loop; empty list otherwise.
*/
private List<BlockItemNode> getForLoopIncrementors(LoopContractBlock loop) {
List<BlockItemNode> result = new LinkedList<>();
if (isForLoop(loop.getLoopNode())) {
ForLoopNode forLoop = (ForLoopNode) loop.getLoopNode();
if (forLoop.getIncrementer() != null)
result.add(nodeFactory.newExpressionStatementNode(
forLoop.getIncrementer().copy()));
}
return result;
}
/**
* The non-deterministic branch: one branch goes to the endless while loop
* completing the induction step and the other branch goes to the
* conclusion, i.e., havoc write set nicely, assume invariants hold, etc.
*
* @throws SyntaxException
*/
private BlockItemNode toNDBranch(LoopContractBlock loop,
List<BlockItemNode> inductionStep) throws SyntaxException {
ExpressionNode bnd = createNDBinaryChoice();
StatementNode inductionBranch, concludeBranch;
Source inductionStepSource = joinSource(inductionStep);
inductionBranch = nodeFactory
.newCompoundStatementNode(inductionStepSource, inductionStep);
// build conclusion branch ...
List<BlockItemNode> concludeBranchComponents = new LinkedList<>();
concludeBranchComponents.addAll(getForLoopInitializers(loop));
concludeBranchComponents.addAll(createConclusion(loop, null));
concludeBranch = nodeFactory.newCompoundStatementNode(
joinSource(concludeBranchComponents), concludeBranchComponents);
Source source = joinSource(
Arrays.asList(bnd, inductionBranch, concludeBranch));
return nodeFactory.newIfNode(source, bnd, inductionBranch,
concludeBranch);
}
/**
* <p>
* Depending on whether <code>writeSetName</code> is <code>null</code>, the
* returned code is slightly different.
* </p>
*
* <p>
* If<code>writeSetName</code> is <code>null</code>,<code>loop</code> must
* have non-empty loop-assigns. Returning <code>
*
* $mem_havoc([loop-assigns]);
* $assume([loop-inv] && ![loop-cond]);
*
* </code>
* </p>
*
* <p>
* If<code>writeSetName</code> is <code>non-null</code>, returning <code>
*
* $mem_havoc(writeSetName);
* $assume([loop-inv] && ![loop-cond]);
*
* </code>
* </p>
*/
private List<BlockItemNode> createConclusion(LoopContractBlock loop,
String writeSetName) {
List<BlockItemNode> result = new LinkedList<>();
if (writeSetName == null) {
assert !loop.getLoopAssignSet().isEmpty();
String tmpWsName = nextLoopTmpIdentifier();
result.add(memTypeVariableDeclaration(tmpWsName));
result.addAll(unionLoopAssigns(loop.getLoopAssignSet(), tmpWsName));
result.addAll(createMemHavoc(tmpWsName));
} else {
result.addAll(createMemHavoc(writeSetName));
}
// assuming (loop-inv && !loop-cond && sidecond) holds:
ExpressionNode loopInv = loop.getLoopInvariants(nodeFactory);
ExpressionNode loopCond = loop.getLoopNode().getCondition();
ExpressionNode notLoopCond = nodeFactory.newOperatorNode(
loopCond.getSource(), Operator.NOT, loopCond.copy());
Source finalAssumeSource = joinSource(
Arrays.asList(loopInv, notLoopCond));
ExpressionNode assumption = nodeFactory.newOperatorNode(
finalAssumeSource, Operator.LAND, loopInv.copy(), notLoopCond);
result.add(assumeNode(assumption));
return result;
}
/**
* @return <code>while(1);</code>
*/
private List<BlockItemNode> endlessWhileLoop() throws SyntaxException {
Source source = this.newSource("while(1);", CivlcTokenConstant.WHILE);
Source trueSource = this.newSource("1", CivlcTokenConstant.CONST);
return Arrays.asList(nodeFactory.newWhileLoopNode(source,
nodeFactory.newIntegerConstantNode(trueSource, "1"),
nodeFactory.newNullStatementNode(source), null));
}
/* *********************** Utility methods ****************************** */
/**
* $mem_havoc(m);
*/
private List<BlockItemNode> createMemHavoc(String varName) {
List<BlockItemNode> results = new LinkedList<>();
String funcName;
List<ExpressionNode> args;
ExpressionNode call, m = identifierExpression(varName);
funcName = MEM_HAVOC;
args = Arrays.asList(m);
call = nodeFactory.newFunctionCallNode(m.getSource(),
identifierExpression(funcName), args, null);
results.add(nodeFactory.newExpressionStatementNode(call));
return results;
}
private BlockItemNode memTypeVariableDeclaration(String name) {
Source source = newSource("$mem " + name,
CivlcTokenConstant.DECLARATION);
return nodeFactory.newVariableDeclarationNode(source, identifier(name),
nodeFactory.newMemTypeNode(source));
}
private StatementNode createAssignment(ExpressionNode lhs,
ExpressionNode rhs) {
Source source = newSource(
lhs.prettyRepresentation() + " = " + rhs.prettyRepresentation(),
CivlcTokenConstant.ASSIGN);
return nodeFactory.newExpressionStatementNode(
nodeFactory.newOperatorNode(source, Operator.ASSIGN, lhs, rhs));
}
/**
* <code>
* $assert($mem_contains(loopAssignsUnionName, write_set));
* </code>
*
* @throws SyntaxException
*
*/
private List<BlockItemNode> checkFrameCondition(String writeSetName,
String loopAssignsUnionName) throws SyntaxException {
Source mcSource = newSource(MEM_CONTAINS, CivlcTokenConstant.CALL);
List<BlockItemNode> results = new LinkedList<>();
// assert
ExpressionNode call = nodeFactory.newFunctionCallNode(mcSource,
identifierExpression(MEM_CONTAINS),
Arrays.asList(identifierExpression(loopAssignsUnionName),
identifierExpression(writeSetName)),
null);
results.add(createAssertion(call, 1));
return results;
}
/**
* <code>
* writeSet = $mem_union(loopAssigns<sub>0</sub>,
* loopAssigns<sub>1</sub>,
* ...,
* loopAssigns<sub>n-1</sub>);
* </code>
*/
private List<BlockItemNode> unionLoopAssigns(
List<ExpressionNode> loopAssigns, String writeSetName) {
Source muSource = newSource(MEM_UNION, CivlcTokenConstant.CALL);
Source meSource = newSource(MEM_EMPTY, CivlcTokenConstant.CALL);
List<BlockItemNode> results = new LinkedList<>();
// init to empty
results.add(createAssignment(identifierExpression(writeSetName),
nodeFactory.newFunctionCallNode(meSource,
identifierExpression(MEM_EMPTY), Arrays.asList(),
null)));
// executes union:
for (ExpressionNode loopAssignsArg : loopAssigns) {
ExpressionNode addrOf = nodeFactory.newOperatorNode(
loopAssignsArg.getSource(), Operator.ADDRESSOF,
loopAssignsArg.copy());
ExpressionNode unionCall = nodeFactory.newFunctionCallNode(muSource,
identifierExpression(MEM_UNION),
Arrays.asList(identifierExpression(writeSetName), addrOf),
null);
results.add(createAssignment(identifierExpression(writeSetName),
unionCall));
}
return results;
}
/**
* <code>$mem_unary_widening(memVarName)</code>
*/
@SuppressWarnings("unused")
private BlockItemNode createMemWidening(String memVarName) {
Source source = newSource(MEM_UNARY_WIDENING, CivlcTokenConstant.CALL);
return nodeFactory.newExpressionStatementNode(
functionCall(source, MEM_UNARY_WIDENING,
Arrays.asList(this.identifierExpression(memVarName))));
}
/**
* <code>lhs = $mem_unary_widening($mem_union(operand1, operand2))</code>
*/
private BlockItemNode createMemUnionWidening(String lhs, String operand1,
String operand2) {
Source unionSource = newSource(MEM_UNION, CivlcTokenConstant.CALL);
ExpressionNode unionNode = functionCall(unionSource, MEM_UNION,
Arrays.asList(identifierExpression(operand1),
identifierExpression(operand2)));
Source wideningsource = newSource(MEM_UNARY_WIDENING,
CivlcTokenConstant.CALL);
ExpressionNode wideningNode = functionCall(wideningsource,
MEM_UNARY_WIDENING, Arrays.asList(unionNode));
return createAssignment(identifierExpression(lhs), wideningNode);
}
@SuppressWarnings("unused")
private BlockItemNode createMemUnionWidening2(String lhs, String operand1,
String operand2) {
Source unionSource = newSource(MEM_UNION_WIDENING,
CivlcTokenConstant.CALL);
ExpressionNode unionNode = functionCall(unionSource, MEM_UNION_WIDENING,
Arrays.asList(identifierExpression(operand1),
identifierExpression(operand2)));
return createAssignment(identifierExpression(lhs), unionNode);
}
/**
* <code>$mem_empty()</code> expression
*/
private ExpressionNode createMemEmptyCall() {
Source source = newSource(MEM_EMPTY, CivlcTokenConstant.CALL);
ExpressionNode callNode = functionCall(source, MEM_EMPTY,
Arrays.asList());
return callNode;
}
/**
* <code>lhs = $mem_havoc_sidecond(writeSet)</code>
*/
@SuppressWarnings("unused")
@Deprecated
private BlockItemNode createMemHavocSidecond(String lhs,
String writeSetName) {
Source source = newSource(MEM_HAVOC_SIDECOND, CivlcTokenConstant.CALL);
ExpressionNode callNode = functionCall(source, MEM_HAVOC_SIDECOND,
Arrays.asList(identifierExpression(writeSetName)));
return createAssignment(identifierExpression(lhs), callNode);
}
/**
* Creates an assertion function call with an argument "predicate".
*
* @param predicate
* The {@link ExpressionNode} which represents a predicate. It is
* the only argument of an assertion call.
* @param kind
* an integer indicating the kind of error message, there are 3
* options: 0: establishment violation; 1: frame-condition
* violation; 2: loop invariant preservation violation
* @return A created assert call statement node;
* @throws SyntaxException
*/
private StatementNode createAssertion(ExpressionNode predicate, int kind)
throws SyntaxException {
ExpressionNode assertIdentifier = identifierExpression(
BaseWorker.ASSERT);
Source source = newSource("$assert", CivlcTokenConstant.CALL);
String errMsg = kind == 0
? establishViolationMessage
: kind == 1 ? frameConditionViolationMessage : violationMessage;
CivlcToken errMsgToken = kind == 0
? loopInvariantsEstablishViolationMessageToken
: kind == 1
? frameConditionViolationMessageToken
: loopInvariantsViolationMessageToken;
StringLiteralNode messageNode = nodeFactory.newStringLiteralNode(source,
errMsg, astFactory.getTokenFactory().newStringToken(errMsgToken)
.getStringLiteral());
FunctionCallNode assertCall = nodeFactory.newFunctionCallNode(source,
assertIdentifier, Arrays.asList(predicate.copy(), messageNode),
null);
return nodeFactory.newExpressionStatementNode(assertCall);
}
/**
* Creates an assume_push function call with an argument "predicate".
*
* @param predicate
* The {@link ExpressionNode} which represents a predicate. It is
* the only argument of an assumption call.
* @return A created assumption call statement node;
*/
private StatementNode createAssumptionPush(ExpressionNode predicate) {
ExpressionNode assumeIdentifier = identifierExpression(ASSUME_PUSH);
FunctionCallNode assumeCall = nodeFactory.newFunctionCallNode(
predicate.getSource(), assumeIdentifier,
Arrays.asList(predicate.copy()), null);
return nodeFactory.newExpressionStatementNode(assumeCall);
}
/**
* Creates an assume_pop function call.
*
* @return A created assumption call statement node;
*/
private StatementNode createAssumptionPop() {
Source source = newSource(ASSUME_POP, CivlcTokenConstant.CALL);
ExpressionNode assumeIdentifier = identifierExpression(ASSUME_POP);
FunctionCallNode assumeCall = nodeFactory.newFunctionCallNode(source,
assumeIdentifier, Arrays.asList(), null);
return nodeFactory.newExpressionStatementNode(assumeCall);
}
/**
*
* @return a <code>$write_set_push()</code> statement node;
*/
private StatementNode createWriteSetPush() {
Source source = this.newSource("$write_set_push",
CivlcTokenConstant.CALL);
ExpressionNode wsPushIdentifier = identifierExpression(WRITE_SET_PUSH);
FunctionCallNode wsPushCall = nodeFactory.newFunctionCallNode(source,
wsPushIdentifier, Arrays.asList(), null);
return nodeFactory.newExpressionStatementNode(wsPushCall);
}
/**
* <code>
* lhs = $write_set_pop();
* </code>
*/
private BlockItemNode createWriteSetPop(String lhs) {
Source writeSetPop = newSource(WRITE_SET_POP, CivlcTokenConstant.CALL);
return createAssignment(identifierExpression(lhs),
nodeFactory.newFunctionCallNode(writeSetPop,
identifierExpression(WRITE_SET_POP), Arrays.asList(),
null));
}
/**
* @return <code>$choose_int(2)</code> call.
* @throws SyntaxException
*/
private ExpressionNode createNDBinaryChoice() throws SyntaxException {
Source source = newSource("$choose_int(2)", CivlcTokenConstant.CALL);
return nodeFactory.newFunctionCallNode(source,
identifierExpression(CHOOSE_INT),
Arrays.asList(nodeFactory.newIntegerConstantNode(source, "2")),
null);
}
/**
* combines {@link Source}s of a list of iterable of AST nodes.
*/
private Source joinSource(Iterable<? extends ASTNode> nodes) {
Source result = null;
for (ASTNode node : nodes) {
result = result == null
? node.getSource()
: tokenFactory.join(result, node.getSource());
}
if (result == null)
result = newSource("", CivlcTokenConstant.ABSENT);
return result;
}
}