Skip to content

Commit

Permalink
unsupported initializer
Browse files Browse the repository at this point in the history
  • Loading branch information
csanadtelbisz committed Nov 1, 2023
1 parent ff9a9ef commit 9d51f37
Show file tree
Hide file tree
Showing 10 changed files with 182 additions and 45 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
package hu.bme.mit.theta.frontend.transformation.grammar.expression;

import hu.bme.mit.theta.core.model.Valuation;
import hu.bme.mit.theta.core.type.LitExpr;
import hu.bme.mit.theta.core.type.NullaryExpr;
import hu.bme.mit.theta.core.type.inttype.IntType;

import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;

public class UnsupportedInitializer extends NullaryExpr<IntType> {

@Override
public IntType getType() {
return Int();
}

@Override
public LitExpr<IntType> eval(Valuation val) {
throw new UnsupportedOperationException("UnsupportedInitializer expressions are not supported.");
}

@Override
public String toString() {
return "UnsupportedInitializer";
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,11 @@
import hu.bme.mit.theta.c.frontend.dsl.gen.CBaseVisitor;
import hu.bme.mit.theta.c.frontend.dsl.gen.CParser;
import hu.bme.mit.theta.frontend.ParseContext;
import hu.bme.mit.theta.frontend.transformation.grammar.expression.UnsupportedInitializer;
import hu.bme.mit.theta.frontend.transformation.grammar.function.FunctionVisitor;
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.TypedefVisitor;
import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration;
import hu.bme.mit.theta.frontend.transformation.model.statements.CExpr;
import hu.bme.mit.theta.frontend.transformation.model.statements.CInitializerList;
import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement;
import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType;
Expand Down Expand Up @@ -81,13 +83,17 @@ public List<CDeclaration> getDeclarations(CParser.DeclarationSpecifiersContext d
"Initializer list designators not yet implemented!");
CInitializerList cInitializerList = new CInitializerList(
cSimpleType.getActualType(), parseContext);
for (CParser.InitializerContext initializer : context.initializer()
.initializerList().initializers) {
CStatement expr = initializer.assignmentExpression()
.accept(functionVisitor);
cInitializerList.addStatement(null /* TODO: add designator */, expr);
try {
for (CParser.InitializerContext initializer : context.initializer()
.initializerList().initializers) {
CStatement expr = initializer.assignmentExpression().accept(functionVisitor);
cInitializerList.addStatement(null /* TODO: add designator */, expr);
}
initializerExpression = cInitializerList;
} catch (NullPointerException e) {
initializerExpression = new CExpr(new UnsupportedInitializer(), parseContext);
parseContext.getMetadata().create(initializerExpression.getExpression(), "cType", cSimpleType);
}
initializerExpression = cInitializerList;
} else {
initializerExpression = context.initializer().assignmentExpression()
.accept(functionVisitor);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ private fun List<VarAccessMap>.mergeAndCollect(): VarAccessMap = this.fold(mapOf
* Returns the list of accessed variables by the label.
* The variable is associated with true if the variable is written and false otherwise.
*/
internal fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) {
fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) {
is StmtLabel -> {
when (stmt) {
is HavocStmt<*> -> mapOf(stmt.varDecl to WRITE)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -113,21 +113,18 @@ class XcfaProcedureBuilder @JvmOverloads constructor(
}

fun addParam(toAdd: VarDecl<*>, dir: ParamDirection) {
check(
!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
params.add(Pair(toAdd, dir))
vars.add(toAdd)
}

fun addVar(toAdd: VarDecl<*>) {
check(
!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
vars.add(toAdd)
}

fun removeVar(toRemove: VarDecl<*>) {
check(
!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
vars.remove(toRemove)
}

Expand Down Expand Up @@ -159,8 +156,7 @@ class XcfaProcedureBuilder @JvmOverloads constructor(
}

fun addEdge(toAdd: XcfaEdge) {
check(
!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
addLoc(toAdd.source)
addLoc(toAdd.target)
edges.add(toAdd)
Expand All @@ -169,8 +165,7 @@ class XcfaProcedureBuilder @JvmOverloads constructor(
}

fun addLoc(toAdd: XcfaLocation) {
check(
!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
if (!locs.contains(toAdd)) {
check(!toAdd.error)
check(!toAdd.initial)
Expand All @@ -180,31 +175,27 @@ class XcfaProcedureBuilder @JvmOverloads constructor(
}

fun removeEdge(toRemove: XcfaEdge) {
check(
!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
toRemove.source.outgoingEdges.remove(toRemove)
toRemove.target.incomingEdges.remove(toRemove)
edges.remove(toRemove)
}

fun removeLoc(toRemove: XcfaLocation) {
check(
!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
locs.remove(toRemove)
}

fun removeLocs(pred: (XcfaLocation) -> Boolean) {
check(
!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
while (locs.any(pred)) {
locs.removeIf(pred)
edges.removeIf { pred(it.source) }
}
}

fun changeVars(varLut: Map<VarDecl<*>, VarDecl<*>>) {
check(
!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" }
val savedVars = ArrayList(vars)
vars.clear()
savedVars.forEach { vars.add(checkNotNull(varLut[it])) }
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,22 @@ import hu.bme.mit.theta.frontend.transformation.grammar.expression.Reference
import hu.bme.mit.theta.xcfa.model.*

/**
* Transforms the following pthread procedure calls into model elements:
* - pthread_create()
* - pthread_join()
* Transforms the library procedure calls with names in supportedFunctions into model elements.
* Requires the ProcedureBuilder be `deterministic`.
*/
class PthreadFunctionsPass(val parseContext: ParseContext) : ProcedurePass {
class CLibraryFunctionsPass(val parseContext: ParseContext) : ProcedurePass {

private val supportedFunctions = setOf(
"printf",
"pthread_join",
"pthread_create",
"pthread_mutex_lock",
"pthread_mutex_unlock",
"pthread_cond_wait",
"pthread_cond_signal",
"pthread_mutex_init",
"pthread_cond_init"
)

override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder {
checkNotNull(builder.metaData["deterministic"])
Expand All @@ -42,7 +52,8 @@ class PthreadFunctionsPass(val parseContext: ParseContext) : ProcedurePass {
if (predicate((it.label as SequenceLabel).labels[0])) {
val invokeLabel = it.label.labels[0] as InvokeLabel
val metadata = invokeLabel.metadata
val fences: List<XcfaLabel> = when (invokeLabel.name) {
val labels: List<XcfaLabel> = when (invokeLabel.name) {
"printf" -> listOf(NopLabel)
"pthread_join" -> {
var handle = invokeLabel.params[1]
while (handle is Reference<*, *>) handle = handle.op
Expand Down Expand Up @@ -107,10 +118,10 @@ class PthreadFunctionsPass(val parseContext: ParseContext) : ProcedurePass {

"pthread_mutex_init", "pthread_cond_init" -> listOf(NopLabel)

else -> error("Unknown pthread function ${invokeLabel.name}")
else -> error("Unsupported library function ${invokeLabel.name}")
}
edge.withLabel(SequenceLabel(fences)).splitIf { fence ->
fence is FenceLabel && fence.labels.any { l -> l.startsWith("start_cond_wait") }
edge.withLabel(SequenceLabel(labels)).splitIf { label ->
label is FenceLabel && label.labels.any { l -> l.startsWith("start_cond_wait") }
}.forEach(builder::addEdge)
} else {
builder.addEdge(edge.withLabel(SequenceLabel(it.label.labels)))
Expand All @@ -122,6 +133,6 @@ class PthreadFunctionsPass(val parseContext: ParseContext) : ProcedurePass {
}

private fun predicate(it: XcfaLabel): Boolean {
return it is InvokeLabel && it.name.startsWith("pthread_")
return it is InvokeLabel && it.name in supportedFunctions
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -27,14 +27,15 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext) : ProcedurePas
// removing redundant elements
EmptyEdgeRemovalPass(parseContext),
UnusedLocRemovalPass(parseContext),
// optimizing
SimplifyExprsPass(parseContext),
// handling intrinsics
ErrorLocationPass(checkOverflow, parseContext),
FinalLocationPass(checkOverflow, parseContext),
SvCompIntrinsicsPass(parseContext),
FpFunctionsToExprsPass(parseContext),
PthreadFunctionsPass(parseContext),
CLibraryFunctionsPass(parseContext),
// optimizing
// UnusedWriteRemovalPass(),
SimplifyExprsPass(parseContext),
LoopUnrollPass(),
// trying to inline procedures
InlineProceduresPass(parseContext),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,10 @@ import hu.bme.mit.theta.core.utils.StmtUtils
import hu.bme.mit.theta.core.utils.TypeUtils.cast
import hu.bme.mit.theta.frontend.ParseContext
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
Expand All @@ -46,6 +49,7 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass {

override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder {
checkNotNull(builder.metaData["deterministic"])
removeUnusedGlobalVarWrites(builder)
val valuation = findConstVariables(builder)
val edges = LinkedHashSet(builder.getEdges())
for (edge in edges) {
Expand Down Expand Up @@ -82,6 +86,26 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass {
return builder
}

private fun removeUnusedGlobalVarWrites(builder: XcfaProcedureBuilder) {
val usedVars = mutableSetOf<VarDecl<*>>()
val xcfaBuilder = builder.parent
xcfaBuilder.getProcedures().flatMap { it.getEdges() }.forEach {
it.label.collectVarsWithAccessType().forEach { (varDecl, access) ->
if (access.isRead) usedVars.add(varDecl)
}
}
val unusedVars = xcfaBuilder.getVars().map { it.wrappedVar } union builder.getVars() subtract
usedVars subtract builder.getParams().map { it.first }.toSet()
System.err.println("Unused vars: $unusedVars")
xcfaBuilder.getProcedures().forEach { b ->
b.getEdges().toList().forEach { edge ->
val newLabel = edge.label.removeUnusedWrites(unusedVars)
b.removeEdge(edge)
b.addEdge(edge.withLabel(newLabel))
}
}
}

private fun findConstVariables(builder: XcfaProcedureBuilder): Valuation {
val valuation = MutableValuation()
builder.parent.getProcedures()
Expand All @@ -100,7 +124,10 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass {
}
.filterNotNull()
.forEach { assignment ->
valuation.put(assignment.varDecl, assignment.expr.eval(ImmutableValuation.empty()))
try {
valuation.put(assignment.varDecl, assignment.expr.eval(ImmutableValuation.empty()))
} catch (_: UnsupportedOperationException) {
}
}
return valuation
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
/*
* 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.xcfa.passes

import hu.bme.mit.theta.core.decl.VarDecl
import hu.bme.mit.theta.core.stmt.AssignStmt
import hu.bme.mit.theta.core.stmt.HavocStmt
import hu.bme.mit.theta.xcfa.collectVarsWithAccessType
import hu.bme.mit.theta.xcfa.isRead
import hu.bme.mit.theta.xcfa.model.*

/**
* Remove unused writes from the program.
* Requires the ProcedureBuilder to be `deterministic` (@see DeterministicPass)
*/
class UnusedWriteRemovalPass : ProcedurePass {

override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder {
checkNotNull(builder.metaData["deterministic"])

val usedVars = mutableSetOf<VarDecl<*>>()
builder.getEdges().forEach {
it.label.collectVarsWithAccessType().forEach { (varDecl, access) ->
if (access.isRead) usedVars.add(varDecl)
}
}
val unusedVars = builder.getVars() subtract usedVars subtract builder.getParams().map { it.first }.toSet()

builder.getEdges().toList().forEach { edge ->
val newLabel = edge.label.removeUnusedWrites(unusedVars)
builder.removeEdge(edge)
builder.addEdge(edge.withLabel(newLabel))
}

return builder
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -29,12 +29,6 @@ import hu.bme.mit.theta.xcfa.getFlatLabels
import hu.bme.mit.theta.xcfa.model.*
import java.util.*

fun label2edge(edge: XcfaEdge, label: XcfaLabel) {
val source = edge.source
val target = edge.target

}

/**
* XcfaEdge must be in a `deterministic` ProcedureBuilder
*/
Expand Down Expand Up @@ -154,4 +148,34 @@ private fun XcfaProcedureBuilder.canInline(tally: LinkedList<String>): Boolean {
tally.pop()
metaData[if (recursive) "recursive" else "canInline"] = Unit
return !recursive
}

internal fun XcfaLabel.removeUnusedWrites(unusedVars: Set<VarDecl<*>>): XcfaLabel {
return when (this) {
is SequenceLabel -> {
val newLabels = mutableListOf<XcfaLabel>()
this.labels.forEach { label ->
val newLabel = label.removeUnusedWrites(unusedVars)
if (newLabel !is NopLabel) newLabels.add(newLabel)
}
SequenceLabel(newLabels)
}

is NondetLabel -> {
val newLabels = mutableSetOf<XcfaLabel>()
this.labels.forEach { label ->
val newLabel = label.removeUnusedWrites(unusedVars)
if (newLabel !is NopLabel) newLabels.add(newLabel)
}
NondetLabel(newLabels)
}

is StmtLabel -> when (this.stmt) {
is AssignStmt<*> -> if (unusedVars.contains(this.stmt.varDecl)) NopLabel else this
is HavocStmt<*> -> if (unusedVars.contains(this.stmt.varDecl)) NopLabel else this
else -> this
}

else -> this
}
}
Loading

0 comments on commit 9d51f37

Please sign in to comment.