@@ -41,9 +41,11 @@ import cpp
4141
4242/** Used to represent the hash-cons of an expression. */
4343private cached newtype HCBase =
44- HC_IntConst ( int val , Type t ) { mk_IntConst ( val , t , _) }
44+ HC_IntLiteral ( int val , Type t ) { mk_IntLiteral ( val , t , _) }
4545 or
46- HC_FloatConst ( float val , Type t ) { mk_FloatConst ( val , t , _) }
46+ HC_FloatLiteral ( float val , Type t ) { mk_FloatLiteral ( val , t , _) }
47+ or
48+ HC_StringLiteral ( string val , Type t ) { mk_StringLiteral ( val , t , _) }
4749 or
4850 HC_Variable ( Variable x ) {
4951 mk_Variable ( x , _)
@@ -106,8 +108,9 @@ class HC extends HCBase {
106108
107109 /** Gets the kind of the HC. This can be useful for debugging. */
108110 string getKind ( ) {
109- if this instanceof HC_IntConst then result = "IntConst" else
110- if this instanceof HC_FloatConst then result = "FloatConst" else
111+ if this instanceof HC_IntLiteral then result = "IntLiteral" else
112+ if this instanceof HC_FloatLiteral then result = "FloatLiteral" else
113+ if this instanceof HC_StringLiteral then result = "StringLiteral" else
111114 if this instanceof HC_Variable then result = "Variable" else
112115 if this instanceof HC_FieldAccess then result = "FieldAccess" else
113116 if this instanceof HC_Deref then result = "Deref" else
@@ -144,33 +147,45 @@ class HC extends HCBase {
144147 }
145148}
146149
147- private predicate analyzableIntConst ( Expr e ) {
150+ private predicate analyzableIntLiteral ( Literal e ) {
148151 strictcount ( e .getValue ( ) .toInt ( ) ) = 1 and
149152 strictcount ( e .getType ( ) .getUnspecifiedType ( ) ) = 1
150153}
151154
152- private predicate mk_IntConst ( int val , Type t , Expr e ) {
153- analyzableIntConst ( e ) and
155+ private predicate mk_IntLiteral ( int val , Type t , Expr e ) {
156+ analyzableIntLiteral ( e ) and
154157 val = e .getValue ( ) .toInt ( ) and
155- t = e .getType ( ) .getUnspecifiedType ( )
158+ t = e .getType ( ) .getUnspecifiedType ( ) and
159+ t instanceof IntegralType
156160}
157-
158- private predicate analyzableFloatConst ( Expr e ) {
161+ private predicate analyzableFloatLiteral ( Literal e ) {
159162 strictcount ( e .getValue ( ) .toFloat ( ) ) = 1 and
160- strictcount ( e .getType ( ) .getUnspecifiedType ( ) ) = 1 and
161- not analyzableIntConst ( e )
163+ strictcount ( e .getType ( ) .getUnspecifiedType ( ) ) = 1
162164}
163165
164- private predicate mk_FloatConst ( float val , Type t , Expr e ) {
165- analyzableFloatConst ( e ) and
166+ private predicate mk_FloatLiteral ( float val , Type t , Expr e ) {
167+ analyzableFloatLiteral ( e ) and
166168 val = e .getValue ( ) .toFloat ( ) and
167- t = e .getType ( ) .getUnspecifiedType ( )
169+ t = e .getType ( ) .getUnspecifiedType ( ) and
170+ t instanceof FloatingPointType
171+ }
172+
173+ private predicate analyzableStringLiteral ( Literal e ) {
174+ strictcount ( e .getValue ( ) ) = 1 and
175+ strictcount ( e .getType ( ) .getUnspecifiedType ( ) ) = 1
176+ }
177+
178+ private predicate mk_StringLiteral ( string val , Type t , Expr e ) {
179+ analyzableStringLiteral ( e ) and
180+ val = e .getValue ( ) and
181+ t = e .getType ( ) .getUnspecifiedType ( ) and
182+ t .( ArrayType ) .getBaseType ( ) instanceof CharType
183+
168184}
169185
170186private predicate analyzableDotFieldAccess ( DotFieldAccess access ) {
171187 strictcount ( access .getTarget ( ) ) = 1 and
172- strictcount ( access .getQualifier ( ) .getFullyConverted ( ) ) = 1 and
173- not analyzableConst ( access )
188+ strictcount ( access .getQualifier ( ) .getFullyConverted ( ) ) = 1
174189}
175190
176191private predicate mk_DotFieldAccess (
@@ -182,8 +197,7 @@ private predicate mk_DotFieldAccess(
182197
183198private predicate analyzablePointerFieldAccess ( PointerFieldAccess access ) {
184199 strictcount ( access .getTarget ( ) ) = 1 and
185- strictcount ( access .getQualifier ( ) .getFullyConverted ( ) ) = 1 and
186- not analyzableConst ( access )
200+ strictcount ( access .getQualifier ( ) .getFullyConverted ( ) ) = 1
187201}
188202
189203private predicate mk_PointerFieldAccess (
@@ -208,8 +222,7 @@ private predicate mk_PointerFieldAccess_with_deref(
208222private predicate analyzableImplicitThisFieldAccess (
209223 ImplicitThisFieldAccess access ) {
210224 strictcount ( access .getTarget ( ) ) = 1 and
211- strictcount ( access .getEnclosingFunction ( ) ) = 1 and
212- not analyzableConst ( access )
225+ strictcount ( access .getEnclosingFunction ( ) ) = 1
213226}
214227
215228private predicate mk_ImplicitThisFieldAccess (
@@ -238,8 +251,7 @@ private predicate mk_ImplicitThisFieldAccess_with_deref(
238251
239252private predicate analyzableVariable ( VariableAccess access ) {
240253 not ( access instanceof FieldAccess ) and
241- strictcount ( access .getTarget ( ) ) = 1 and
242- not analyzableConst ( access )
254+ strictcount ( access .getTarget ( ) ) = 1
243255}
244256
245257private predicate mk_Variable ( Variable x , VariableAccess access ) {
@@ -249,8 +261,7 @@ private predicate mk_Variable(Variable x, VariableAccess access) {
249261
250262private predicate analyzableConversion ( Conversion conv ) {
251263 strictcount ( conv .getType ( ) .getUnspecifiedType ( ) ) = 1 and
252- strictcount ( conv .getExpr ( ) ) = 1 and
253- not analyzableConst ( conv )
264+ strictcount ( conv .getExpr ( ) ) = 1
254265}
255266
256267private predicate mk_Conversion ( Type t , HC child , Conversion conv ) {
@@ -263,8 +274,7 @@ private predicate analyzableBinaryOp(BinaryOperation op) {
263274 op .isPure ( ) and
264275 strictcount ( op .getLeftOperand ( ) .getFullyConverted ( ) ) = 1 and
265276 strictcount ( op .getRightOperand ( ) .getFullyConverted ( ) ) = 1 and
266- strictcount ( op .getOperator ( ) ) = 1 and
267- not analyzableConst ( op )
277+ strictcount ( op .getOperator ( ) ) = 1
268278}
269279
270280private predicate mk_BinaryOp (
@@ -279,8 +289,7 @@ private predicate analyzableUnaryOp(UnaryOperation op) {
279289 not ( op instanceof PointerDereferenceExpr ) and
280290 op .isPure ( ) and
281291 strictcount ( op .getOperand ( ) .getFullyConverted ( ) ) = 1 and
282- strictcount ( op .getOperator ( ) ) = 1 and
283- not analyzableConst ( op )
292+ strictcount ( op .getOperator ( ) ) = 1
284293}
285294
286295private predicate mk_UnaryOp ( HC child , string opname , UnaryOperation op ) {
@@ -290,8 +299,7 @@ private predicate mk_UnaryOp(HC child, string opname, UnaryOperation op) {
290299}
291300
292301private predicate analyzableThisExpr ( ThisExpr thisExpr ) {
293- strictcount ( thisExpr .getEnclosingFunction ( ) ) = 1 and
294- not analyzableConst ( thisExpr )
302+ strictcount ( thisExpr .getEnclosingFunction ( ) ) = 1
295303}
296304
297305private predicate mk_ThisExpr ( Function fcn , ThisExpr thisExpr ) {
@@ -301,8 +309,7 @@ private predicate mk_ThisExpr(Function fcn, ThisExpr thisExpr) {
301309
302310private predicate analyzableArrayAccess ( ArrayExpr ae ) {
303311 strictcount ( ae .getArrayBase ( ) .getFullyConverted ( ) ) = 1 and
304- strictcount ( ae .getArrayOffset ( ) .getFullyConverted ( ) ) = 1 and
305- not analyzableConst ( ae )
312+ strictcount ( ae .getArrayOffset ( ) .getFullyConverted ( ) ) = 1
306313}
307314
308315private predicate mk_ArrayAccess (
@@ -314,8 +321,7 @@ private predicate mk_ArrayAccess(
314321
315322private predicate analyzablePointerDereferenceExpr (
316323 PointerDereferenceExpr deref ) {
317- strictcount ( deref .getOperand ( ) .getFullyConverted ( ) ) = 1 and
318- not analyzableConst ( deref )
324+ strictcount ( deref .getOperand ( ) .getFullyConverted ( ) ) = 1
319325}
320326
321327private predicate mk_Deref (
@@ -327,12 +333,16 @@ private predicate mk_Deref(
327333/** Gets the hash-cons of expression `e`. */
328334cached HC hashCons ( Expr e ) {
329335 exists ( int val , Type t
330- | mk_IntConst ( val , t , e ) and
331- result = HC_IntConst ( val , t ) )
336+ | mk_IntLiteral ( val , t , e ) and
337+ result = HC_IntLiteral ( val , t ) )
332338 or
333339 exists ( float val , Type t
334- | mk_FloatConst ( val , t , e ) and
335- result = HC_FloatConst ( val , t ) )
340+ | mk_FloatLiteral ( val , t , e ) and
341+ result = HC_FloatLiteral ( val , t ) )
342+ or
343+ exists ( string val , Type t
344+ | mk_StringLiteral ( val , t , e ) and
345+ result = HC_StringLiteral ( val , t ) )
336346 or
337347 // Variable with no SSA information.
338348 exists ( Variable x
@@ -377,20 +387,16 @@ cached HC hashCons(Expr e) {
377387 or
378388 ( not analyzableExpr ( e , _) and result = HC_Unanalyzable ( e ) )
379389}
380-
381- private predicate analyzableConst ( Expr e ) {
382- analyzableIntConst ( e ) or
383- analyzableFloatConst ( e )
384- }
385-
386390/**
387391 * Holds if the expression is explicitly handled by `hashCons`.
388392 * Unanalyzable expressions still need to be given a hash-cons,
389393 * but it will be a unique number that is not shared with any other
390394 * expression.
391395 */
392396predicate analyzableExpr ( Expr e , string kind ) {
393- ( analyzableConst ( e ) and kind = "Const" ) or
397+ ( analyzableIntLiteral ( e ) and kind = "IntLiteral" ) or
398+ ( analyzableFloatLiteral ( e ) and kind = "FloatLiteral" ) or
399+ ( analyzableStringLiteral ( e ) and kind = "StringLiteral" ) or
394400 ( analyzableDotFieldAccess ( e ) and kind = "DotFieldAccess" ) or
395401 ( analyzablePointerFieldAccess ( e ) and kind = "PointerFieldAccess" ) or
396402 ( analyzableImplicitThisFieldAccess ( e ) and kind = "ImplicitThisFieldAccess" ) or
0 commit comments