diff --git a/config/openbsd--memorysafety.properties b/config/openbsd--memorysafety.properties new file mode 100644 index 0000000000..2017992154 --- /dev/null +++ b/config/openbsd--memorysafety.properties @@ -0,0 +1,51 @@ +# ---------------------------------------------------------------------- +# This configuration file uses a combination of value analysis +# and symbolic memory graphs to verify memory safety properties. +# ---------------------------------------------------------------------- +log.level = FINER +# specification to find memory related problems +specification = specification/sv-comp-memorysafety.spc + +cpa = cpa.arg.ARGCPA +ARGCPA.cpa = cpa.composite.CompositeCPA +CompositeCPA.cpas = cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.functionpointer.FunctionPointerCPA, cpa.smg.SMGCPA + +# checking conterexamples, esp. with CBMC does not make sense +analysis.checkCounterexamples = false + +analysis.traversal.order = dfs +analysis.traversal.useReversePostorder = false +analysis.traversal.useCallstack = false + +cpa.smg.enableMallocFail = false +cpa.smg.handleUnknownFunctions = assume_safe +cpa.smg.guessSizeOfUnknownMemorySize = false +cpa.smg.trackPredicates = true +cpa.smg.verifyPredicates = true + +cpa.composite.aggregateBasicBlocks = false + +# The file to which the witness is written (required by competition). +counterexample.export.graphml = witness.graphml +cpa.arg.proofWitness = witness.graphml +# Compression is not supported by UltimateAutomizer +counterexample.export.compressWitness = false +cpa.arg.compressWitness = false + +# simplified CFA is bad for witnesses +cfa.simplifyCfa = false + +# This is the configuration used when verifying memory safety properties (actually this configuration). +memorysafety.config = openbsd--memorysafety.properties + +# Memory allocation functions +cpa.smg.memoryAllocationFunctions = malloc + +# Array allocation functions +cpa.smg.arrayAllocationFunctions = mallocarray + +# Allocation functions which set memory to zero +cpa.smg.zeroingMemoryAllocation = __builtin_memset + +# Deallocation functions +cpa.smg.deallocationFunctions = free diff --git a/config/openbsd--smg.properties b/config/openbsd--smg.properties new file mode 100644 index 0000000000..ac854156e1 --- /dev/null +++ b/config/openbsd--smg.properties @@ -0,0 +1,80 @@ +# +# CPAchecker is a tool for configurable software verification. +# This file is part of CPAchecker. +# +# Copyright (C) 2007-2018 Dirk Beyer +# All rights reserved. +# +# 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. +# +# +# CPAchecker web page: +# http://cpachecker.sosy-lab.org +# + +#include includes/valueAnalysis.properties +log.level = FINE + +# specification to find memory related problems +specification = specification/memorysafety.spc, specification/TerminatingFunctions.spc + +CompositeCPA.cpas = cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.functionpointer.FunctionPointerCPA, cpa.smg.SMGCPA + +# checking conterexamples, esp. with CBMC does not make sense +analysis.checkCounterexamples = false + +analysis.traversal.order = bfs +analysis.traversal.useReversePostorder = false +analysis.traversal.useCallstack = false +analysis.traversal.useLoopstack = true + +cpa.smg.enableMallocFail = false +cpa.smg.handleUnknownFunctions = assume_safe +cpa.smg.guessSizeOfUnknownMemorySize = true +cpa.smg.trackPredicates = true +cpa.smg.verifyPredicates = true +cpa.smg.exportSMGwhen = NEVER +cpa.smg.exportSMG.file = smg-%s.dot +cpa.smg.handleExternVariableAsExternalAllocation = true +cpa.smg.handleUnknownDereferenceAsSafe = true +cpa.smg.enableHeapAbstraction = true +# print coverage info to file despite output.disable=false +coverage.file = coverage.info + +cpa.smg.GCCZeroLengthArray = true +cpa.smg.stop = END_BLOCK +cpa.composite.aggregateBasicBlocks = false + +cpa.arg.witness.removeInsufficientEdges = false + +# simplified CFA is bad for witnesses +cfa.simplifyCfa = false + +# Ignore function calls by pointer if the value of pointer variable is not known by FunctionPointerCPA +cpa.functionpointer.ignoreUnknownFunctionPointerCalls=true + +parser.readLineDirectives = true +# This is the configuration used when verifying memory safety properties (actually this configuration). +memorysafety.config = openbsd--smg.properties + +# Memory allocation functions +cpa.smg.memoryAllocationFunctions = malloc + +# Array allocation functions +cpa.smg.arrayAllocationFunctions = mallocarray + +# Allocation functions which set memory to zero +cpa.smg.zeroingMemoryAllocation = __builtin_memset + +# Deallocation functions +cpa.smg.deallocationFunctions = free diff --git a/doc/ConfigurationOptions.txt b/doc/ConfigurationOptions.txt index 89b2205274..9ee969ebf2 100644 --- a/doc/ConfigurationOptions.txt +++ b/doc/ConfigurationOptions.txt @@ -1937,7 +1937,7 @@ cpa.predicate.memoryAllocationFunctions = { # Memory allocation functions of which all parameters but the first should be # ignored. cpa.predicate.memoryAllocationFunctionsWithSuperfluousParameters = { - "__kmalloc", "kmalloc", "kzalloc"} + "__kmalloc", "kmalloc", "kzalloc", "malloc"} # Set of functions that non-deterministically provide new zeroed memory on # the heap, i.e. they can return either a valid pointer or zero. diff --git a/src/org/sosy_lab/cpachecker/cfa/ast/c/CVariableDeclaration.java b/src/org/sosy_lab/cpachecker/cfa/ast/c/CVariableDeclaration.java index d29b721943..3efd58ac35 100644 --- a/src/org/sosy_lab/cpachecker/cfa/ast/c/CVariableDeclaration.java +++ b/src/org/sosy_lab/cpachecker/cfa/ast/c/CVariableDeclaration.java @@ -56,7 +56,6 @@ public final class CVariableDeclaration extends AVariableDeclaration implements checkArgument(!(cStorageClass == CStorageClass.EXTERN && getInitializer() != null), "Extern declarations cannot have an initializer"); checkArgument(cStorageClass == CStorageClass.EXTERN || cStorageClass == CStorageClass.AUTO, "CStorageClass is %s", cStorageClass); - checkArgument(pIsGlobal || cStorageClass == CStorageClass.AUTO); checkArgument( cStorageClass == CStorageClass.EXTERN || !(pType.getCanonicalType() instanceof CVoidType), "Cannot declare variable of type void: %s", diff --git a/src/org/sosy_lab/cpachecker/cfa/parser/eclipse/c/ASTConverter.java b/src/org/sosy_lab/cpachecker/cfa/parser/eclipse/c/ASTConverter.java index 2ad79e9c80..929ff1759c 100644 --- a/src/org/sosy_lab/cpachecker/cfa/parser/eclipse/c/ASTConverter.java +++ b/src/org/sosy_lab/cpachecker/cfa/parser/eclipse/c/ASTConverter.java @@ -1678,9 +1678,10 @@ class ASTConverter { } if (!isGlobal && cStorageClass == CStorageClass.EXTERN) { - // TODO: implement this, it "imports" the externally declared variable - // into the scope of this block. - throw parseContext.parseError("Local variable declared extern is unsupported", d); + // TODO: EXTERN variables without global scope can be viewed as + // global if they are only accessed in the local scope. But this is + // only a work around. + isGlobal = true; } if (!isGlobal && scope.variableNameInUse(name)) { diff --git a/src/org/sosy_lab/cpachecker/cpa/smg/SMGTransferRelation.java b/src/org/sosy_lab/cpachecker/cpa/smg/SMGTransferRelation.java index 4e5a34e8e4..eaec7e45f6 100644 --- a/src/org/sosy_lab/cpachecker/cpa/smg/SMGTransferRelation.java +++ b/src/org/sosy_lab/cpachecker/cpa/smg/SMGTransferRelation.java @@ -829,7 +829,7 @@ public class SMGTransferRelation String varName = pVarDecl.getName(); CType cType = TypeUtils.getRealExpressionType(pVarDecl); - if (cType.isIncomplete() && cType instanceof CElaboratedType) { + if (cType.isIncomplete() && (cType instanceof CElaboratedType ||cType instanceof CArrayType)) { // for incomplete types, we do not add variables. // we are not allowed to read or write them, dereferencing is possible. // example: "struct X; extern struct X var; void main() { }" @@ -847,9 +847,13 @@ public class SMGTransferRelation int typeSize = expressionEvaluator.getBitSizeof(pEdge, cType, pState); // Handle incomplete type of extern variables as externally allocated - if (options.isHandleExternVariableAsExternalAllocation() && cType.isIncomplete() && - pVarDecl.getCStorageClass().equals(CStorageClass.EXTERN)) { - typeSize = options.getExternalAllocationSize(); + if (cType.isIncomplete() && pVarDecl.getCStorageClass().equals(CStorageClass.EXTERN)) { + if (options.isHandleExternVariableAsExternalAllocation()) { + // XXX what if the size is defined later in this file? + typeSize = options.getExternalAllocationSize(); + } else { + return ImmutableList.of(pState); + } } if (pVarDecl.isGlobal()) { newObject = pState.addGlobalVariable(typeSize, varName); @@ -883,17 +887,15 @@ public class SMGTransferRelation if (newInitializer != null) { return handleInitializer(pState, pVarDecl, pEdge, pObject, 0, cType, newInitializer); + } else if (pVarDecl.getCStorageClass().equals(CStorageClass.EXTERN)) { + if (options.isHandleExternVariableAsExternalAllocation()) { + // Don't nullify extern variables + pState.setExternallyAllocatedFlag(pObject); + } } else if (pVarDecl.isGlobal()) { - // Don't nullify extern variables - if (pVarDecl.getCStorageClass().equals(CStorageClass.EXTERN)) { - if (options.isHandleExternVariableAsExternalAllocation()) { - pState.setExternallyAllocatedFlag(pObject); - } - } else { - // Global variables without initializer are nullified in C + // Global variables without initializer are nullified in C pState = expressionEvaluator.writeValue(pState, pObject, 0, cType, SMGZeroValue.INSTANCE, pEdge); - } } return ImmutableList.of(pState); diff --git a/src/org/sosy_lab/cpachecker/util/predicates/pathformula/SSAMap.java b/src/org/sosy_lab/cpachecker/util/predicates/pathformula/SSAMap.java index f0bdde8b42..efb4aa636d 100644 --- a/src/org/sosy_lab/cpachecker/util/predicates/pathformula/SSAMap.java +++ b/src/org/sosy_lab/cpachecker/util/predicates/pathformula/SSAMap.java @@ -37,6 +37,7 @@ import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap; import org.sosy_lab.common.collect.PersistentSortedMap; import org.sosy_lab.common.collect.PersistentSortedMaps; import org.sosy_lab.common.collect.PersistentSortedMaps.MergeConflictHandler; +import org.sosy_lab.cpachecker.cfa.types.c.CArrayType; import org.sosy_lab.cpachecker.cfa.types.c.CComplexType; import org.sosy_lab.cpachecker.cfa.types.c.CComplexType.ComplexTypeKind; import org.sosy_lab.cpachecker.cfa.types.c.CElaboratedType; @@ -65,12 +66,21 @@ public class SSAMap implements Serializable { Preconditions.checkArgument( (type1 instanceof CFunctionType && type2 instanceof CFunctionType) || (isEnumPointerType(type1) && isEnumPointerType(type2)) - || type1.equals(type2), + || type1.equals(type2) + || (type1 instanceof CArrayType && type2 instanceof CArrayType), "Cannot change type of variable %s in SSAMap from %s to %s", name, type1, type2); + if ((type2 instanceof CArrayType) && ((CArrayType) type2).getLength() != null) { + // If type2 is an array with initialization and it contains + // members, return it. Otherwise return type1. + // There are previous checks to make sure only one of type1 and + // type2 can be initialized. + return type2; + } + return type1; } diff --git a/src/org/sosy_lab/cpachecker/util/predicates/pathformula/pointeraliasing/DynamicMemoryHandler.java b/src/org/sosy_lab/cpachecker/util/predicates/pathformula/pointeraliasing/DynamicMemoryHandler.java index 73e6592cdc..d0ab33e6f1 100644 --- a/src/org/sosy_lab/cpachecker/util/predicates/pathformula/pointeraliasing/DynamicMemoryHandler.java +++ b/src/org/sosy_lab/cpachecker/util/predicates/pathformula/pointeraliasing/DynamicMemoryHandler.java @@ -188,14 +188,8 @@ class DynamicMemoryHandler { parameters = Collections.singletonList(multiplication); } - } else if (parameters.size() != 1) { - if (parameters.size() > 1 && conv.options.hasSuperfluousParameters(functionName)) { + } else { parameters = Collections.singletonList(parameters.get(0)); - } else { - throw new UnrecognizedCodeException( - String.format("Memory allocation function %s() called with %d parameters instead of 1", - functionName, parameters.size()), edge, e); - } } final String delegateFunctionName = !isZeroing ? @@ -330,12 +324,10 @@ class DynamicMemoryHandler { * @throws UnrecognizedCodeException If the C code was unrecognizable. */ private Value handleMemoryFree(final CFunctionCallExpression e, - final CExpressionVisitorWithPointerAliasing expressionVisitor) throws UnrecognizedCodeException { - final List parameters = e.getParameterExpressions(); - if (parameters.size() != 1) { - throw new UnrecognizedCodeException( - String.format("free() called with %d parameters", parameters.size()), edge, e); - } + final CExpressionVisitorWithPointerAliasing expressionVisitor) + throws UnrecognizedCodeException { + List parameters = e.getParameterExpressions(); + parameters = Collections.singletonList(parameters.get(0)); if (errorConditions.isEnabled()) { final Formula operand = diff --git a/src/org/sosy_lab/cpachecker/util/predicates/pathformula/pointeraliasing/FormulaEncodingWithPointerAliasingOptions.java b/src/org/sosy_lab/cpachecker/util/predicates/pathformula/pointeraliasing/FormulaEncodingWithPointerAliasingOptions.java index c2224d1bbd..bd06e440b4 100644 --- a/src/org/sosy_lab/cpachecker/util/predicates/pathformula/pointeraliasing/FormulaEncodingWithPointerAliasingOptions.java +++ b/src/org/sosy_lab/cpachecker/util/predicates/pathformula/pointeraliasing/FormulaEncodingWithPointerAliasingOptions.java @@ -36,7 +36,7 @@ public class FormulaEncodingWithPointerAliasingOptions extends FormulaEncodingOp @Option(secure=true, description = "Memory allocation functions of which all parameters but the first should be ignored.") private ImmutableSet memoryAllocationFunctionsWithSuperfluousParameters = ImmutableSet.of( - "__kmalloc", "kmalloc", "kzalloc"); + "__kmalloc", "kmalloc", "kzalloc", "malloc"); @Option(secure=true, description = "The function used to model successful heap object allocation. " + "This is only used, when pointer analysis with UFs is enabled.")