-
Notifications
You must be signed in to change notification settings - Fork 29
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Add IntrinsicsInlining * Added new nondet_loop.c code + unit test. --------- Co-authored-by: Thomas Haas <[email protected]>
- Loading branch information
1 parent
0dd7003
commit 037ba25
Showing
8 changed files
with
16,342 additions
and
65 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,17 @@ | ||
| #include <stdint.h> | ||
| #include <assert.h> | ||
|
|
||
| int main() | ||
| { | ||
| int x = 0; | ||
| while (x != 5) { | ||
| if (__VERIFIER_nondet_int() == 0) { | ||
| x += 2; | ||
| } else { | ||
| x += 3; | ||
| } | ||
| } | ||
| assert (0); | ||
|
|
||
| return 0; | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
115 changes: 115 additions & 0 deletions
115
dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IntrinsicsInlining.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,115 @@ | ||
| package com.dat3m.dartagnan.program.processing; | ||
|
|
||
| import com.dat3m.dartagnan.exception.ParsingException; | ||
| import com.dat3m.dartagnan.expression.BNonDet; | ||
| import com.dat3m.dartagnan.expression.Expression; | ||
| import com.dat3m.dartagnan.expression.ExpressionFactory; | ||
| import com.dat3m.dartagnan.expression.INonDet; | ||
| import com.dat3m.dartagnan.expression.type.BooleanType; | ||
| import com.dat3m.dartagnan.expression.type.IntegerType; | ||
| import com.dat3m.dartagnan.expression.type.TypeFactory; | ||
| import com.dat3m.dartagnan.program.Program; | ||
| import com.dat3m.dartagnan.program.Register; | ||
| import com.dat3m.dartagnan.program.Thread; | ||
| import com.dat3m.dartagnan.program.event.EventFactory; | ||
| import com.dat3m.dartagnan.program.event.core.Event; | ||
| import com.dat3m.dartagnan.program.event.functions.DirectFunctionCall; | ||
| import com.dat3m.dartagnan.program.event.functions.DirectValueFunctionCall; | ||
| import com.google.common.primitives.UnsignedInteger; | ||
| import com.google.common.primitives.UnsignedLong; | ||
| import org.sosy_lab.common.configuration.Configuration; | ||
| import org.sosy_lab.common.configuration.InvalidConfigurationException; | ||
|
|
||
| import java.math.BigInteger; | ||
| import java.util.List; | ||
|
|
||
| public class IntrinsicsInlining implements ProgramProcessor { | ||
|
|
||
| private int constantId; | ||
|
|
||
| private IntrinsicsInlining() { | ||
| } | ||
|
|
||
| public static IntrinsicsInlining fromConfig(Configuration ignored) throws InvalidConfigurationException { | ||
| return new IntrinsicsInlining(); | ||
| } | ||
|
|
||
| @Override | ||
| public void run(Program program) { | ||
| constantId = 0; | ||
| for (Thread thread : program.getThreads()) { | ||
| run(thread); | ||
| } | ||
| } | ||
|
|
||
| private void run(Thread thread) { | ||
| for (DirectFunctionCall call : thread.getEvents(DirectFunctionCall.class)) { | ||
| assert !call.getCallTarget().hasBody(); | ||
|
|
||
| List<Event> replacement = switch (call.getCallTarget().getName()) { | ||
| case "__VERIFIER_nondet_bool", | ||
| "__VERIFIER_nondet_int", "__VERIFIER_nondet_uint", "__VERIFIER_nondet_unsigned_int", | ||
| "__VERIFIER_nondet_short", "__VERIFIER_nondet_ushort", "__VERIFIER_nondet_unsigned_short", | ||
| "__VERIFIER_nondet_long", "__VERIFIER_nondet_ulong", | ||
| "__VERIFIER_nondet_char", "__VERIFIER_nondet_uchar" -> inlineNonDet(call); | ||
| default -> throw new UnsupportedOperationException( | ||
| String.format("Undefined function %s", call.getCallTarget().getName())); | ||
| }; | ||
|
|
||
| replacement.forEach(e -> e.copyAllMetadataFrom(call)); | ||
| call.replaceBy(replacement); | ||
| } | ||
| } | ||
|
|
||
| private List<Event> inlineNonDet(DirectFunctionCall call) { | ||
| TypeFactory types = TypeFactory.getInstance(); | ||
| ExpressionFactory expressions = ExpressionFactory.getInstance(); | ||
| assert call instanceof DirectValueFunctionCall; | ||
| Register register = ((DirectValueFunctionCall) call).getResultRegister(); | ||
| String name = call.getCallTarget().getName(); | ||
| final String separator = "nondet_"; | ||
| int index = name.indexOf(separator); | ||
| assert index > -1; | ||
| String suffix = name.substring(index + separator.length()); | ||
|
|
||
| // Nondeterministic booleans | ||
| if (suffix.equals("bool")) { | ||
| BooleanType booleanType = types.getBooleanType(); | ||
| var nondeterministicExpression = new BNonDet(booleanType); | ||
| Expression cast = expressions.makeCast(nondeterministicExpression, register.getType()); | ||
| return List.of(EventFactory.newLocal(register, cast)); | ||
| } | ||
|
|
||
| // Nondeterministic integers | ||
| boolean signed = switch (suffix) { | ||
| case "int", "short", "long", "char" -> true; | ||
| default -> false; | ||
| }; | ||
| final BigInteger min = switch (suffix) { | ||
| case "long" -> BigInteger.valueOf(Long.MIN_VALUE); | ||
| case "int" -> BigInteger.valueOf(Integer.MIN_VALUE); | ||
| case "short" -> BigInteger.valueOf(Short.MIN_VALUE); | ||
| case "char" -> BigInteger.valueOf(Byte.MIN_VALUE); | ||
| default -> BigInteger.ZERO; | ||
| }; | ||
| final BigInteger max = switch (suffix) { | ||
| case "int" -> BigInteger.valueOf(Integer.MAX_VALUE); | ||
| case "uint", "unsigned_int" -> UnsignedInteger.MAX_VALUE.bigIntegerValue(); | ||
| case "short" -> BigInteger.valueOf(Short.MAX_VALUE); | ||
| case "ushort", "unsigned_short" -> BigInteger.valueOf(65535); | ||
| case "long" -> BigInteger.valueOf(Long.MAX_VALUE); | ||
| case "ulong" -> UnsignedLong.MAX_VALUE.bigIntegerValue(); | ||
| case "char" -> BigInteger.valueOf(Byte.MAX_VALUE); | ||
| case "uchar" -> BigInteger.valueOf(255); | ||
| default -> throw new UnsupportedOperationException(String.format("%s is not supported", call)); | ||
| }; | ||
| if (!(register.getType() instanceof IntegerType type)) { | ||
| throw new ParsingException(String.format("Non-integer result register %s.", register)); | ||
| } | ||
| var expression = new INonDet(constantId++, type, signed); | ||
| expression.setMin(min); | ||
| expression.setMax(max); | ||
| call.getFunction().getProgram().addConstant(expression); | ||
| return List.of(EventFactory.newLocal(register, expression)); | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.