Skip to content

Commit

Permalink
Merge branch 'development' into devirt_pthread
Browse files Browse the repository at this point in the history
  • Loading branch information
@ThomasHaas
ThomasHaas authored Dec 18, 2023
2 parents b9fe795 + f924058 commit 3761771
Show file tree
Hide file tree
Showing 5 changed files with 185 additions and 74 deletions.
125 changes: 63 additions & 62 deletions dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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";
}
8 changes: 6 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down
Loading

0 comments on commit 3761771

Please sign in to comment.