@@ -371,10 +371,13 @@ abstract class RegexString extends Expr {
371371 or
372372 // octal value \ooo
373373 end in [ start + 2 .. start + 4 ] and
374- this .getText ( ) .substring ( start + 1 , end ) .toInt ( ) >= 0 and
374+ // this.isOctal([start + 1 .. end]) and
375+ forall ( int i | i in [ start + 1 .. end - 1 ] | this .isOctal ( i ) ) and
376+ // this.getText().substring(start + 1, end).toInt() >= 0 and
375377 not (
376378 end < start + 4 and
377- exists ( this .getText ( ) .substring ( start + 1 , end + 1 ) .toInt ( ) )
379+ this .isOctal ( end ) //and
380+ // exists(this.getText().substring(start + 1, end + 1).toInt())
378381 )
379382 or
380383 // 16-bit hex value \uhhhh
@@ -392,6 +395,11 @@ abstract class RegexString extends Expr {
392395 )
393396 }
394397
398+ pragma [ inline]
399+ private predicate isOctal ( int index ) {
400+ this .getChar ( index ) in [ "0" , "1" , "2" , "3" , "4" , "5" , "6" , "7" ]
401+ }
402+
395403 /** Holds if `index` is inside a character set. */
396404 predicate inCharSet ( int index ) {
397405 exists ( int x , int y | this .charSet ( x , y ) and index in [ x + 1 .. y - 2 ] )
@@ -690,6 +698,7 @@ abstract class RegexString extends Expr {
690698
691699 private predicate numbered_backreference ( int start , int end , int value ) {
692700 this .escapingChar ( start ) and
701+ // starting with 0 makes it an octal escape
693702 not this .getChar ( start + 1 ) = "0" and
694703 exists ( string text , string svalue , int len |
695704 end = start + len and
@@ -698,8 +707,18 @@ abstract class RegexString extends Expr {
698707 |
699708 svalue = text .substring ( start + 1 , start + len ) and
700709 value = svalue .toInt ( ) and
701- not exists ( text .substring ( start + 1 , start + len + 1 ) .toInt ( ) ) and
702- value > 0
710+ // value is composed of digits
711+ forall ( int i | i in [ start + 1 .. start + len - 1 ] |
712+ this .getChar ( i ) in [ "0" , "1" , "2" , "3" , "4" , "5" , "6" , "7" , "8" , "9" ]
713+ ) and
714+ // a longer reference is not possible
715+ not (
716+ len = 2 and
717+ exists ( text .substring ( start + 1 , start + len + 1 ) .toInt ( ) )
718+ ) and
719+ // 3 octal digits makes it an octal escape
720+ not forall ( int i | i in [ start + 1 .. start + 4 ] | this .isOctal ( i ) )
721+ // TODO: Inside a character set, all numeric escapes are treated as characters.
703722 )
704723 }
705724
0 commit comments