Support quantifiers in ACSL #704
Conversation
.../de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/MainDispatcher.java
Show resolved
Hide resolved
...ltimate/cdt/translation/implementation/base/expressiontranslation/ExpressionTranslation.java
Outdated
Show resolved
Hide resolved
| final CType cType = AcslTypeUtils.translateAcslTypeToCType(decl.getType()); | ||
| final DeclarationInformation declInfo = new DeclarationInformation(StorageClass.QUANTIFIED, null); | ||
| final BoogieType boogieType = mTypeHandler.getBoogieTypeForCType(cType); | ||
| // TODO: Handle quantified variables on heap |
There was a problem hiding this comment.
What exactly does this mean, and what would have to be done?
There was a problem hiding this comment.
Actually I don't know 😄
This wold happen, if we quantify over pointers and I am not sure about the ACSL semantics in that case.
Also, I don't think we support pointer types in ACSL properly, so we would probably crash earlier.
So maybe I can just replace the TODO with a comment that we don't support pointers for now and thus yield a LocalLValue.
There was a problem hiding this comment.
I am also confused what "quantified variables on heap" means. Is this a quantified pointer?
But I agree, that sounds rather difficult. Perhaps we should crash as soon as we encounter it, i.e., throw UnsupportedSyntax .
There was a problem hiding this comment.
I just replaced this TODO with an exception. I don't think it can be triggered for now, as we already crash before for non-primitive types (definitely in AcslTypeUtils::translateAcslTypeToCType, maybe already during parsing). But this may change in the future and the thrown exception also serves as some form of documentation.
...src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ACSLHandler.java
Outdated
Show resolved
Hide resolved
|
Regarding the test cases: I wanted to wait for #703 to write some tests with quantifiers over arrays, but I will just add some simple tests to demonstrate the basic functionality, |
| final CType cType = AcslTypeUtils.translateAcslTypeToCType(decl.getType()); | ||
| final DeclarationInformation declInfo = new DeclarationInformation(StorageClass.QUANTIFIED, null); | ||
| final BoogieType boogieType = mTypeHandler.getBoogieTypeForCType(cType); | ||
| // TODO: Handle quantified variables on heap |
There was a problem hiding this comment.
I am also confused what "quantified variables on heap" means. Is this a quantified pointer?
But I agree, that sounds rather difficult. Perhaps we should crash as soon as we encounter it, i.e., throw UnsupportedSyntax .
schuessf
force-pushed
the
wip/fs/acsl-quantifiers
branch
2 times, most recently
from
ca48b46 to
d288eb8
Compare
...k/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java
Show resolved
Hide resolved
| @@ -121,7 +121,7 @@ public enum RedirectionStrategy { | |||
| public static final boolean DEF_USESEPARATETRACECHECKSOLVER = true; | |||
| public static final SolverMode DEF_CHOOSESEPARATETRACECHECKSOLVER = SolverMode.Internal_SMTInterpol; | |||
| public static final String DEF_SEPARATETRACECHECKSOLVERCOMMAND = ""; | |||
| public static final String DEF_SEPARATETRACECHECKSOLVERTHEORY = "QF_AUFLIA"; | |||
| public static final String DEF_SEPARATETRACECHECKSOLVERTHEORY = "ALL"; | |||
There was a problem hiding this comment.
Is it really intended to change the default setting here? If so, are there any settings files that also need to be adapted?
There was a problem hiding this comment.
In all the relevant settings (e.g. for SV-COMP) ALL was already used. The most simple solution to fix the failing test would be of course to just adapt the settings files that is responsible for the tests. However, to be consistent with Automizer (see RcfgPreferenceInitializer), I adapted the default setting for Kojak instead, but maybe this is nothing that should be done in this PR.
* Introduce ScopedHashMap for quantified variables and use it for the handling of IdentifierExpressions * Use type constraints in Boogie-quantifiers (with implication for \forall and "and" for \exists)
Otherwise the tests with quantifiers fail
schuessf
force-pushed
the
wip/fs/acsl-quantifiers
branch
from
7253c6b to
e4645c2
Compare
This PR adds support for quantifiers in ACSL.
NotDefinedExpression. There was also a AST object for aQuantifierExpressionthat I just adapted to our needs.ACSLHandler. The crucial steps in this translation are that we have to handle the quantified variables in the expression inside the quantifier properly (track the variables in aScopedHashMapand first lookup when handling anIdentifierExpression) and that we add type constraints over the quantified variables (ACSL may use bounded types that are translated to an unbounded type in Boogie).Note that we can only handle quantified expressions, where the inner expressions is side-effect free (which also does not allow any auxiliary statements). Therefore, quantified expressions that contain dereferences are currently not supported, but this should be fixed in #703.