C++: uniqueness fixes for HashCons

This commit is contained in:
Robert Marsh
2018-08-27 11:38:16 -07:00
parent 3a5eb03055
commit 91da02bacf
3 changed files with 38 additions and 12 deletions

View File

@@ -47,6 +47,8 @@ private cached newtype HCBase =
or
HC_StringLiteral(string val, Type t) {mk_StringLiteral(val,t,_)}
or
HC_Nullptr() {mk_Nullptr(_)}
or
HC_Variable(Variable x) {
mk_Variable(x, _)
}
@@ -167,30 +169,42 @@ class HC extends HCBase {
private predicate analyzableIntLiteral(Literal e) {
strictcount (e.getValue().toInt()) = 1 and
strictcount (e.getType().getUnspecifiedType()) = 1
strictcount (e.getType().getUnspecifiedType()) = 1 and
e.getType().getUnspecifiedType() instanceof IntegralType
}
private predicate mk_IntLiteral(int val, Type t, Expr e) {
analyzableIntLiteral(e) and
val = e.getValue().toInt() and
t = e.getType().getUnspecifiedType() and
t instanceof IntegralType
t = e.getType().getUnspecifiedType()
}
private predicate analyzableFloatLiteral(Literal e) {
strictcount (e.getValue().toFloat()) = 1 and
strictcount (e.getType().getUnspecifiedType()) = 1
strictcount (e.getType().getUnspecifiedType()) = 1 and
e.getType().getUnspecifiedType() instanceof FloatingPointType
}
private predicate mk_FloatLiteral(float val, Type t, Expr e) {
analyzableFloatLiteral(e) and
val = e.getValue().toFloat() and
t = e.getType().getUnspecifiedType() and
t instanceof FloatingPointType
t = e.getType().getUnspecifiedType()
}
private predicate analyzableNullptr(NullValue e) {
strictcount (e.getType().getUnspecifiedType()) = 1 and
e.getType() instanceof NullPointerType
}
private predicate mk_Nullptr(Expr e) {
analyzableNullptr(e)
}
private predicate analyzableStringLiteral(Literal e) {
strictcount(e.getValue()) = 1 and
strictcount(e.getType().getUnspecifiedType()) = 1
strictcount(e.getType().getUnspecifiedType()) = 1 and
e.getType().getUnspecifiedType().(ArrayType).getBaseType() instanceof CharType
}
private predicate mk_StringLiteral(string val, Type t, Expr e) {
@@ -348,9 +362,9 @@ private predicate mk_Deref(
private predicate analyzableNonmemberFunctionCall(
FunctionCall fc) {
forall(int i | exists(fc.getArgument(i)) | strictcount(fc.getArgument(i)) = 1) and
forall(int i | exists(fc.getArgument(i)) | strictcount(fc.getArgument(i).getFullyConverted()) = 1) and
strictcount(fc.getTarget()) = 1 and
not fc.getTarget().isMember()
not exists(fc.getQualifier())
}
private predicate mk_NonmemberFunctionCall(
@@ -373,9 +387,9 @@ private predicate mk_NonmemberFunctionCall(
private predicate analyzableMemberFunctionCall(
FunctionCall fc) {
forall(int i | exists(fc.getArgument(i)) | strictcount(fc.getArgument(i)) = 1) and
forall(int i | exists(fc.getArgument(i)) | strictcount(fc.getArgument(i).getFullyConverted()) = 1) and
strictcount(fc.getTarget()) = 1 and
strictcount(fc.getQualifier()) = 1
strictcount(fc.getQualifier().getFullyConverted()) = 1
}
private predicate mk_MemberFunctionCall(
@@ -386,7 +400,7 @@ private predicate mk_MemberFunctionCall(
) {
fc.getTarget() = fcn and
analyzableMemberFunctionCall(fc) and
hashCons(fc.getQualifier()) = qual and
hashCons(fc.getQualifier().getFullyConverted()) = qual and
(
exists(HC head, HC_Args tail |
args = HC_ArgCons(fcn, head, fc.getNumberOfArguments() - 1, tail) and
@@ -490,6 +504,11 @@ cached HC hashCons(Expr e) {
| mk_MemberFunctionCall(fcn, qual, args, e) and
result = HC_MemberFunctionCall(fcn, qual, args)
)
or
(
mk_Nullptr(e) and
result = HC_Nullptr()
)
or
(not analyzableExpr(e,_) and result = HC_Unanalyzable(e))
@@ -504,6 +523,7 @@ predicate analyzableExpr(Expr e, string kind) {
(analyzableIntLiteral(e) and kind = "IntLiteral") or
(analyzableFloatLiteral(e) and kind = "FloatLiteral") or
(analyzableStringLiteral(e) and kind = "StringLiteral") or
(analyzableNullptr(e) and kind = "Nullptr") or
(analyzableDotFieldAccess(e) and kind = "DotFieldAccess") or
(analyzablePointerFieldAccess(e) and kind = "PointerFieldAccess") or
(analyzableImplicitThisFieldAccess(e) and kind = "ImplicitThisFieldAccess") or

View File

@@ -66,3 +66,4 @@
| test.cpp:150:3:150:3 | x | 150:c3-c3 150:c9-c9 151:c3-c3 151:c9-c9 152:c12-c12 |
| test.cpp:150:3:150:5 | ... ++ | 150:c3-c5 150:c9-c11 151:c3-c5 151:c9-c11 152:c10-c12 |
| test.cpp:150:3:150:11 | ... + ... | 150:c3-c11 151:c3-c11 |
| test.cpp:156:14:156:20 | 0 | 156:c14-c20 156:c3-c9 157:c10-c16 |

View File

@@ -151,3 +151,8 @@ int test10(int x) {
x++ + x++; // same as above
return ++x; // ++x is not the same as x++
}
void* test11() {
nullptr == nullptr;
return nullptr;
}