From f92405850f50960f379ff526cef5b1209ff846f7 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 16 Dec 2023 21:48:41 +0100 Subject: [PATCH] Add support for checking overflow and memory-safety (#589) Signed-off-by: Hernan Ponce de Leon Co-authored-by: Hernan Ponce de Leon --- .../dartagnan/configuration/OptionNames.java | 125 +++++++++--------- .../expression/ExpressionFactory.java | 8 +- .../program/processing/Intrinsics.java | 121 +++++++++++++++-- .../program/processing/ProcessingManager.java | 4 +- .../program/specification/AssertInline.java | 1 + 5 files changed, 185 insertions(+), 74 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index 4d0a3aa00f..4fee717e70 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -2,76 +2,77 @@ public class OptionNames { - // Base Options - public static final String PROPERTY = "property"; - public static final String BOUND = "bound"; - public static final String TARGET = "target"; - public static final String METHOD = "method"; - public static final String SOLVER = "solver"; - public static final String TIMEOUT = "timeout"; - public static final String VALIDATE = "validate"; - public static final String COVERAGE = "coverage"; + // Base Options + public static final String PROPERTY = "property"; + public static final String BOUND = "bound"; + public static final String TARGET = "target"; + public static final String METHOD = "method"; + public static final String SOLVER = "solver"; + public static final String TIMEOUT = "timeout"; + public static final String VALIDATE = "validate"; + public static final String COVERAGE = "coverage"; - // Modeling Options - public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds"; - public static final String RECURSION_BOUND = "modeling.recursionBound"; + // Modeling Options + public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds"; + public static final String RECURSION_BOUND = "modeling.recursionBound"; - // Compilation Options - public static final String USE_RC11_TO_ARCH_SCHEME = "compilation.rc11ToArch"; - public static final String C_TO_POWER_SCHEME = "compilation.cToPower"; + // Compilation Options + public static final String USE_RC11_TO_ARCH_SCHEME = "compilation.rc11ToArch"; + public static final String C_TO_POWER_SCHEME = "compilation.cToPower"; - // Encoding Options - public static final String USE_INTEGERS = "encoding.integers"; - public static final String ENABLE_ACTIVE_SETS = "encoding.activeSets"; - public static final String REDUCE_ACYCLICITY_ENCODE_SETS = "encoding.wmm.reduceAcyclicityEncodeSets"; - public static final String LOCALLY_CONSISTENT = "encoding.locallyConsistent";//TODO also influences RA - public static final String MERGE_CF_VARS = "encoding.mergeCFVars"; - public static final String INITIALIZE_REGISTERS = "encoding.initializeRegisters"; - public static final String BREAK_SYMMETRY_ON = "encoding.symmetry.breakOn"; - public static final String BREAK_SYMMETRY_BY_SYNC_DEGREE = "encoding.symmetry.orderBySyncDegree"; - public static final String IDL_TO_SAT = "encoding.wmm.idl2sat"; + // Encoding Options + public static final String USE_INTEGERS = "encoding.integers"; + public static final String ENABLE_ACTIVE_SETS = "encoding.activeSets"; + public static final String REDUCE_ACYCLICITY_ENCODE_SETS = "encoding.wmm.reduceAcyclicityEncodeSets"; + public static final String LOCALLY_CONSISTENT = "encoding.locallyConsistent";//TODO also influences RA + public static final String MERGE_CF_VARS = "encoding.mergeCFVars"; + public static final String INITIALIZE_REGISTERS = "encoding.initializeRegisters"; + public static final String BREAK_SYMMETRY_ON = "encoding.symmetry.breakOn"; + public static final String BREAK_SYMMETRY_BY_SYNC_DEGREE = "encoding.symmetry.orderBySyncDegree"; + public static final String IDL_TO_SAT = "encoding.wmm.idl2sat"; - // Program Processing Options - public static final String DETERMINISTIC_REORDERING = "program.processing.detReordering"; - public static final String REDUCE_SYMMETRY = "program.processing.reduceSymmetry"; - public static final String CONSTANT_PROPAGATION = "program.processing.constantPropagation"; - public static final String DEAD_ASSIGNMENT_ELIMINATION = "program.processing.dce"; - public static final String DYNAMIC_PURE_LOOP_CUTTING = "program.processing.dplc"; - public static final String PROPAGATE_COPY_ASSIGNMENTS = "program.processing.propagateCopyAssignments"; - - // Program Property Options - public static final String ALIAS_METHOD = "program.analysis.alias"; - public static final String ALWAYS_SPLIT_ON_JUMPS = "program.analysis.cf.alwaysSplitOnJump"; - public static final String MERGE_BRANCHES = "program.analysis.cf.mergeBranches"; + // Program Processing Options + public static final String DETERMINISTIC_REORDERING = "program.processing.detReordering"; + public static final String REDUCE_SYMMETRY = "program.processing.reduceSymmetry"; + public static final String CONSTANT_PROPAGATION = "program.processing.constantPropagation"; + public static final String DEAD_ASSIGNMENT_ELIMINATION = "program.processing.dce"; + public static final String DYNAMIC_PURE_LOOP_CUTTING = "program.processing.dplc"; + public static final String PROPAGATE_COPY_ASSIGNMENTS = "program.processing.propagateCopyAssignments"; + public static final String REMOVE_ASSERTION_OF_TYPE = "program.processing.skipAssertionsOfType"; + + // Program Property Options + public static final String ALIAS_METHOD = "program.analysis.alias"; + public static final String ALWAYS_SPLIT_ON_JUMPS = "program.analysis.cf.alwaysSplitOnJump"; + public static final String MERGE_BRANCHES = "program.analysis.cf.mergeBranches"; - // Memory Model Options - public static final String ENABLE_RELATION_ANALYSIS = "wmm.analysis.relationAnalysis"; - public static final String ENABLE_MUST_SETS = "wmm.analysis.mustSets"; - public static final String ENABLE_EXTENDED_RELATION_ANALYSIS = "wmm.analysis.extendedRelationAnalysis"; + // Memory Model Options + public static final String ENABLE_RELATION_ANALYSIS = "wmm.analysis.relationAnalysis"; + public static final String ENABLE_MUST_SETS = "wmm.analysis.mustSets"; + public static final String ENABLE_EXTENDED_RELATION_ANALYSIS = "wmm.analysis.extendedRelationAnalysis"; - // Refinement Options - public static final String BASELINE = "refinement.baseline"; + // Refinement Options + public static final String BASELINE = "refinement.baseline"; - // SMT solver Options - public static final String PHANTOM_REFERENCES = "solver.z3.usePhantomReferences"; + // SMT solver Options + public static final String PHANTOM_REFERENCES = "solver.z3.usePhantomReferences"; - // Witness Options - public static final String WITNESS_ORIGINAL_PROGRAM_PATH = "witness.originalProgramFilePath"; - public static final String WITNESS_GRAPHVIZ = "witness.graphviz"; + // Witness Options + public static final String WITNESS_ORIGINAL_PROGRAM_PATH = "witness.originalProgramFilePath"; + public static final String WITNESS_GRAPHVIZ = "witness.graphviz"; - // SVCOMP Options - public static final String PROPERTYPATH = "svcomp.property"; - public static final String UMIN = "svcomp.umin"; - public static final String UMAX = "svcomp.umax"; - public static final String STEP = "svcomp.step"; - public static final String SANITIZE = "svcomp.sanitize"; - public static final String OPTIMIZATION = "svcomp.optimization"; - public static final String INTEGER_ENCODING = "svcomp.integerEncoding"; + // SVCOMP Options + public static final String PROPERTYPATH = "svcomp.property"; + public static final String UMIN = "svcomp.umin"; + public static final String UMAX = "svcomp.umax"; + public static final String STEP = "svcomp.step"; + public static final String SANITIZE = "svcomp.sanitize"; + public static final String OPTIMIZATION = "svcomp.optimization"; + public static final String INTEGER_ENCODING = "svcomp.integerEncoding"; - // Debugging Options - public static final String PRINT_PROGRAM_BEFORE_PROCESSING = "printer.beforeProcessing"; - public static final String PRINT_PROGRAM_AFTER_SIMPLIFICATION = "printer.afterSimplification"; - public static final String PRINT_PROGRAM_AFTER_UNROLLING = "printer.afterUnrolling"; - public static final String PRINT_PROGRAM_AFTER_COMPILATION = "printer.afterCompilation"; - public static final String PRINT_PROGRAM_AFTER_PROCESSING = "printer.afterProcessing"; + // Debugging Options + public static final String PRINT_PROGRAM_BEFORE_PROCESSING = "printer.beforeProcessing"; + public static final String PRINT_PROGRAM_AFTER_SIMPLIFICATION = "printer.afterSimplification"; + public static final String PRINT_PROGRAM_AFTER_UNROLLING = "printer.afterUnrolling"; + public static final String PRINT_PROGRAM_AFTER_COMPILATION = "printer.afterCompilation"; + public static final String PRINT_PROGRAM_AFTER_PROCESSING = "printer.afterProcessing"; } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java index 807607d6e8..47da1bc43f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java @@ -97,16 +97,20 @@ public IValue makeValue(BigInteger value, IntegerType type) { return new IValue(value, type); } - public Expression makeCast(Expression expression, Type type) { + public Expression makeCast(Expression expression, Type type, boolean signed) { if (type instanceof BooleanType) { return makeBooleanCast(expression); } if (type instanceof IntegerType integerType) { - return makeIntegerCast(expression, integerType, false); + return makeIntegerCast(expression, integerType, signed); } throw new UnsupportedOperationException(String.format("Cast %s into %s.", expression, type)); } + public Expression makeCast(Expression expression, Type type) { + return makeCast(expression, type, false); + } + public Expression makeConditional(Expression condition, Expression ifTrue, Expression ifFalse) { return new IfExpr(condition, ifTrue, ifFalse); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java index 6354720f5f..69b39ca776 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java @@ -24,12 +24,19 @@ import java.math.BigInteger; import java.util.ArrayList; import java.util.Arrays; +import java.util.EnumSet; import java.util.List; import java.util.Map; import java.util.function.BiPredicate; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.configuration.Option; +import org.sosy_lab.common.configuration.Options; + import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; +import static com.dat3m.dartagnan.configuration.OptionNames.REMOVE_ASSERTION_OF_TYPE; /** * Manages a collection of all functions that the verifier can define itself, @@ -37,10 +44,19 @@ * Also defines the semantics of most intrinsics, * except some thread-library primitives, which are instead defined in {@link ThreadCreation}. */ +@Options public class Intrinsics { private static final Logger logger = LogManager.getLogger(Intrinsics.class); + @Option(name = REMOVE_ASSERTION_OF_TYPE, + description = "Remove assertions of type [user, overflow, invalidderef].", + toUppercase=true, + secure = true) + private EnumSet notToInline = EnumSet.noneOf(AssertionType.class); + + private enum AssertionType { USER, OVERFLOW, INVALIDDEREF } + private static final TypeFactory types = TypeFactory.getInstance(); private static final ExpressionFactory expressions = ExpressionFactory.getInstance(); @@ -56,6 +72,12 @@ private Intrinsics() { public static Intrinsics newInstance() { return new Intrinsics(); } + + public static Intrinsics fromConfig(Configuration config) throws InvalidConfigurationException { + Intrinsics instance = newInstance(); + config.inject(instance); + return instance; + } public ProgramProcessor markIntrinsicsPass() { return this::markIntrinsics; @@ -106,7 +128,7 @@ public enum Info { VERIFIER_SPIN_START("__VERIFIER_spin_start", false, false, true, true, Intrinsics::inlineSpinStart), VERIFIER_SPIN_END("__VERIFIER_spin_end", false, false, true, true, Intrinsics::inlineSpinEnd), VERIFIER_ASSUME("__VERIFIER_assume", false, false, true, true, Intrinsics::inlineAssume), - VERIFIER_ASSERT("__VERIFIER_assert", false, false, false, false, Intrinsics::inlineAssert), + VERIFIER_ASSERT("__VERIFIER_assert", false, false, false, false, Intrinsics::inlineUserAssert), VERIFIER_NONDET(List.of("__VERIFIER_nondet_bool", "__VERIFIER_nondet_int", "__VERIFIER_nondet_uint", "__VERIFIER_nondet_unsigned_int", "__VERIFIER_nondet_short", "__VERIFIER_nondet_ushort", "__VERIFIER_nondet_unsigned_short", @@ -116,6 +138,7 @@ public enum Info { // --------------------------- LLVM --------------------------- LLVM(List.of("llvm.smax", "llvm.umax", "llvm.smin", "llvm.umin", "llvm.ssub.sat", "llvm.usub.sat", "llvm.sadd.sat", "llvm.uadd.sat", // TODO: saturated shifts + "llvm.sadd.with.overflow", "llvm.ssub.with.overflow", "llvm.smul.with.overflow", "llvm.ctlz", "llvm.ctpop"), false, false, true, true, Intrinsics::handleLLVMIntrinsic), LLVM_ASSUME("llvm.assume", false, false, true, true, Intrinsics::inlineLLVMAssume), @@ -141,11 +164,17 @@ public enum Info { STD_MEMCMP("memcmp", false, true, true, false, Intrinsics::inlineMemCmp), STD_MALLOC("malloc", false, false, true, true, Intrinsics::inlineMalloc), STD_FREE("free", true, false, true, true, Intrinsics::inlineAsZero),//TODO support free - STD_ASSERT(List.of("__assert_fail", "__assert_rtn"), false, false, false, true, Intrinsics::inlineAssert), + STD_ASSERT(List.of("__assert_fail", "__assert_rtn"), false, false, false, true, Intrinsics::inlineUserAssert), STD_EXIT("exit", false, false, false, true, Intrinsics::inlineExit), STD_ABORT("abort", false, false, false, true, Intrinsics::inlineExit), STD_IO(List.of("puts", "putchar", "printf"), false, false, true, true, Intrinsics::inlineAsZero), STD_SLEEP("sleep", false, false, true, true, Intrinsics::inlineAsZero), + // --------------------------- UBSAN --------------------------- + UBSAN_OVERFLOW(List.of("__ubsan_handle_add_overflow", "__ubsan_handle_sub_overflow", + "__ubsan_handle_divrem_overflow", "__ubsan_handle_mul_overflow", "__ubsan_handle_negate_overflow"), + false, false, false, true, Intrinsics::inlineIntegerOverflow), + UBSAN_TYPE_MISSMATCH(List.of("__ubsan_handle_type_mismatch_v1"), + false, false, false, true, Intrinsics::inlineInvalidDereference), ; private final List variants; @@ -221,7 +250,6 @@ private void markIntrinsics(Program program) { } private void declareNondetBool(Program program) { - final TypeFactory types = TypeFactory.getInstance(); // used by VisitorLKMM if (program.getFunctionByName("__VERIFIER_nondet_bool").isEmpty()) { final FunctionType type = types.getFunctionType(types.getBooleanType(), List.of()); @@ -359,15 +387,29 @@ private List inlineMalloc(FunctionCall call) { )); } - private List inlineAssert(FunctionCall call) { - ExpressionFactory expressions = ExpressionFactory.getInstance(); + private List inlineAssert(FunctionCall call, AssertionType skip, String errorMsg) { + if(notToInline.contains(skip)) { + return List.of(); + } final Expression condition = expressions.makeFalse(); - final Event assertion = EventFactory.newAssert(condition, "user assertion"); + final Event assertion = EventFactory.newAssert(condition, errorMsg); final Event abort = EventFactory.newAbortIf(expressions.makeTrue()); abort.addTags(Tag.EARLYTERMINATION); return List.of(assertion, abort); } + private List inlineUserAssert(FunctionCall call) { + return inlineAssert(call, AssertionType.USER, "user assertion"); + } + + private List inlineIntegerOverflow(FunctionCall call) { + return inlineAssert(call, AssertionType.OVERFLOW, "integer overflow"); + } + + private List inlineInvalidDereference(FunctionCall call) { + return inlineAssert(call, AssertionType.INVALIDDEREF, "invalid dereference"); + } + // -------------------------------------------------------------------------------------------------------- // LLVM intrinsics @@ -382,6 +424,12 @@ private List handleLLVMIntrinsic(FunctionCall call) { return inlineLLVMCtpop(valueCall); } else if (name.contains("add.sat")) { return inlineLLVMSaturatedAdd(valueCall); + } else if (name.contains("sadd.with.overflow")) { + return inlineLLVMSAddWithOverflow(valueCall); + } else if (name.contains("ssub.with.overflow")) { + return inlineLLVMSSubWithOverflow(valueCall); + } else if (name.contains("smul.with.overflow")) { + return inlineLLVMSMulWithOverflow(valueCall); } else if (name.contains("sub.sat")) { return inlineLLVMSaturatedSub(valueCall); } else if (name.startsWith("llvm.smax") || name.startsWith("llvm.smin") @@ -543,6 +591,65 @@ private List inlineLLVMSaturatedAdd(ValueFunctionCall call) { ); } + private List inlineLLVMSAddWithOverflow(ValueFunctionCall call) { + return inlineLLVMSOpWithOverflow(call, IOpBin.ADD); + } + + private List inlineLLVMSSubWithOverflow(ValueFunctionCall call) { + return inlineLLVMSOpWithOverflow(call, IOpBin.SUB); + } + + private List inlineLLVMSMulWithOverflow(ValueFunctionCall call) { + return inlineLLVMSOpWithOverflow(call, IOpBin.MUL); + } + + private List inlineLLVMSOpWithOverflow(ValueFunctionCall call, IOpBin op) { + final Register resultReg = call.getResultRegister(); + final List arguments = call.getArguments(); + final Expression x = arguments.get(0); + final Expression y = arguments.get(1); + assert x.getType() == y.getType(); + + // The flag expression defined below has the form A & B. + // A is only relevant for integer encoding, B is only relevant for BV encoding. + // Here we do not yet know yet which encoding will be used and thus use both A & B. + // This probably has no noticeable impact on performance. + + // Check for integer encoding + final IntegerType iType = (IntegerType) x.getType(); + final Expression result = expressions.makeBinary(x, op, y); + final Expression rangeCheck = checkIfValueInRangeOfType(result, iType, true); + + // Check for BV encoding. From LLVM's language manual: + // "An operation overflows if, for any values of its operands A and B and for any N larger than + // the operands’ width, ext(A op B) to iN is not equal to (ext(A) to iN) op (ext(B) to iN) where + // ext is sext for signed overflow and zext for unsigned overflow, and op is the + // underlying arithmetic operation."" + final int width = iType.getBitWidth(); + final Expression xExt = expressions.makeCast(x, types.getIntegerType(width + 1), true); + final Expression yExt = expressions.makeCast(y, types.getIntegerType(width + 1), true); + final Expression resultExt = expressions.makeCast(result, types.getIntegerType(width + 1), true); + final Expression bvCheck = expressions.makeEQ(expressions.makeBinary(xExt, op, yExt), resultExt); + + final Expression flag = expressions.makeCast( + expressions.makeNot(expressions.makeAnd(bvCheck, rangeCheck)), + types.getIntegerType(1) + ); + + return List.of( + EventFactory.newLocal(resultReg, expressions.makeConstruct(List.of(result, flag))) + ); + } + + private Expression checkIfValueInRangeOfType(Expression value, IntegerType integerType, boolean signed) { + final Expression minValue = expressions.makeValue(integerType.getMinimumValue(signed), integerType); + final Expression maxValue = expressions.makeValue(integerType.getMaximumValue(signed), integerType); + return expressions.makeAnd( + expressions.makeLTE(minValue, value, true), + expressions.makeLTE(value, maxValue, true) + ); + } + // -------------------------------------------------------------------------------------------------------- // LKMM intrinsics @@ -642,8 +749,6 @@ private void inlineLate(Function function) { } private List inlineNonDet(FunctionCall call) { - TypeFactory types = TypeFactory.getInstance(); - ExpressionFactory expressions = ExpressionFactory.getInstance(); assert call.isDirectCall() && call instanceof ValueFunctionCall; Register register = ((ValueFunctionCall) call).getResultRegister(); String name = call.getCalledFunction().getName(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java index a5b595b8f5..aec3c20e41 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java @@ -74,13 +74,12 @@ public class ProcessingManager implements ProgramProcessor { private ProcessingManager(Configuration config) throws InvalidConfigurationException { config.inject(this); - final Intrinsics intrinsics = Intrinsics.newInstance(); + final Intrinsics intrinsics = Intrinsics.fromConfig(config); final FunctionProcessor sccp = constantPropagation ? SparseConditionalConstantPropagation.fromConfig(config) : null; programProcessors.addAll(Arrays.asList( printBeforeProcessing ? DebugPrint.withHeader("Before processing", Printer.Mode.ALL) : null, intrinsics.markIntrinsicsPass(), GEPToAddition.newInstance(), - RegisterDecomposition.newInstance(), NaiveDevirtualisation.newInstance(), Inlining.fromConfig(config), ProgramProcessor.fromFunctionProcessor( @@ -92,6 +91,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep Simplifier.fromConfig(config) ), Target.FUNCTIONS, true ), + RegisterDecomposition.newInstance(), RemoveDeadFunctions.newInstance(), printAfterSimplification ? DebugPrint.withHeader("After simplification", Printer.Mode.ALL) : null, LoopFormVerification.fromConfig(config), diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertInline.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertInline.java index b5ca92c222..426498302f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertInline.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertInline.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Assert; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager;