hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-29 02:35:15 +02:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #15980 from MathiasVP/guards-lt

Browse Source 
C++: Support `<` reasoning for `switch` statements in Guards library
This commit is contained in:
Mathias Vorreiter Pedersen
2024-03-20 10:40:39 +00:00
committed by GitHub
parent 9179f0bda6 3a7b80da47
commit 7ff2998c88
6 changed files with 309 additions and 42 deletions
Download Patch File Download Diff File Expand all files Collapse all files

70
cpp/ql/test/library-tests/controlflow/guards-ir/tests.expected
View File

@@ -530,19 +530,27 @@ irGuardsCompare
| 7 | 0 < x+0 when CompareGT: ... > ... is true |
| 7 | 0 >= x+0 when CompareGT: ... > ... is false |
| 7 | x < 0+1 when CompareGT: ... > ... is false |
| 7 | x < 1 when CompareGT: ... > ... is false |
| 7 | x >= 0+1 when CompareGT: ... > ... is true |
| 7 | x >= 1 when CompareGT: ... > ... is true |
| 17 | 0 < x+1 when CompareLT: ... < ... is false |
| 17 | 0 >= x+1 when CompareLT: ... < ... is true |
| 17 | 1 < y+0 when CompareGT: ... > ... is true |
| 17 | 1 >= y+0 when CompareGT: ... > ... is false |
| 17 | x < 0 when CompareLT: ... < ... is true |
| 17 | x < 0+0 when CompareLT: ... < ... is true |
| 17 | x >= 0 when CompareLT: ... < ... is false |
| 17 | x >= 0+0 when CompareLT: ... < ... is false |
| 17 | y < 1+1 when CompareGT: ... > ... is false |
| 17 | y < 2 when CompareGT: ... > ... is false |
| 17 | y >= 1+1 when CompareGT: ... > ... is true |
| 17 | y >= 2 when CompareGT: ... > ... is true |
| 26 | 0 < x+0 when CompareGT: ... > ... is true |
| 26 | 0 >= x+0 when CompareGT: ... > ... is false |
| 26 | x < 0+1 when CompareGT: ... > ... is false |
| 26 | x < 1 when CompareGT: ... > ... is false |
| 26 | x >= 0+1 when CompareGT: ... > ... is true |
| 26 | x >= 1 when CompareGT: ... > ... is true |
| 31 | - ... != x+0 when CompareEQ: ... == ... is false |
| 31 | - ... == x+0 when CompareEQ: ... == ... is true |
| 31 | x != -1 when CompareEQ: ... == ... is false |
@@ -551,20 +559,28 @@ irGuardsCompare
| 31 | x == - ...+0 when CompareEQ: ... == ... is true |
| 34 | 10 < j+1 when CompareLT: ... < ... is false |
| 34 | 10 >= j+1 when CompareLT: ... < ... is true |
| 34 | j < 10 when CompareLT: ... < ... is true |
| 34 | j < 10+0 when CompareLT: ... < ... is true |
| 34 | j >= 10 when CompareLT: ... < ... is false |
| 34 | j >= 10+0 when CompareLT: ... < ... is false |
| 42 | 10 < j+1 when CompareLT: ... < ... is false |
| 42 | 10 >= j+1 when CompareLT: ... < ... is true |
| 42 | j < 10 when CompareLT: ... < ... is true |
| 42 | j < 10+0 when CompareLT: ... < ... is true |
| 42 | j >= 10 when CompareLT: ... < ... is false |
| 42 | j >= 10+0 when CompareLT: ... < ... is false |
| 44 | 0 < z+0 when CompareGT: ... > ... is true |
| 44 | 0 >= z+0 when CompareGT: ... > ... is false |
| 44 | z < 0+1 when CompareGT: ... > ... is false |
| 44 | z < 1 when CompareGT: ... > ... is false |
| 44 | z >= 0+1 when CompareGT: ... > ... is true |
| 44 | z >= 1 when CompareGT: ... > ... is true |
| 45 | 0 < y+0 when CompareGT: ... > ... is true |
| 45 | 0 >= y+0 when CompareGT: ... > ... is false |
| 45 | y < 0+1 when CompareGT: ... > ... is false |
| 45 | y < 1 when CompareGT: ... > ... is false |
| 45 | y >= 0+1 when CompareGT: ... > ... is true |
| 45 | y >= 1 when CompareGT: ... > ... is true |
| 58 | 0 != x+0 when CompareEQ: ... == ... is false |
| 58 | 0 < y+1 when CompareLT: ... < ... is false |
| 58 | 0 == x+0 when CompareEQ: ... == ... is true |
@@ -573,7 +589,9 @@ irGuardsCompare
| 58 | x != 0+0 when CompareEQ: ... == ... is false |
| 58 | x == 0 when CompareEQ: ... == ... is true |
| 58 | x == 0+0 when CompareEQ: ... == ... is true |
| 58 | y < 0 when CompareLT: ... < ... is true |
| 58 | y < 0+0 when CompareLT: ... < ... is true |
| 58 | y >= 0 when CompareLT: ... < ... is false |
| 58 | y >= 0+0 when CompareLT: ... < ... is false |
| 75 | 0 != x+0 when CompareEQ: ... == ... is false |
| 75 | 0 == x+0 when CompareEQ: ... == ... is true |
@@ -601,7 +619,9 @@ irGuardsCompare
| 94 | x == 0+0 when CompareNE: ... != ... is false |
| 102 | 10 < j+1 when CompareLT: ... < ... is false |
| 102 | 10 >= j+1 when CompareLT: ... < ... is true |
| 102 | j < 10 when CompareLT: ... < ... is true |
| 102 | j < 10+0 when CompareLT: ... < ... is true |
| 102 | j >= 10 when CompareLT: ... < ... is false |
| 102 | j >= 10+0 when CompareLT: ... < ... is false |
| 109 | 0 != x+0 when CompareEQ: ... == ... is false |
| 109 | 0 < y+1 when CompareLT: ... < ... is false |
@@ -611,7 +631,9 @@ irGuardsCompare
| 109 | x != 0+0 when CompareEQ: ... == ... is false |
| 109 | x == 0 when CompareEQ: ... == ... is true |
| 109 | x == 0+0 when CompareEQ: ... == ... is true |
| 109 | y < 0 when CompareLT: ... < ... is true |
| 109 | y < 0+0 when CompareLT: ... < ... is true |
| 109 | y >= 0 when CompareLT: ... < ... is false |
| 109 | y >= 0+0 when CompareLT: ... < ... is false |
| 156 | ... + ... != x+0 when CompareEQ: ... == ... is false |
| 156 | ... + ... == x+0 when CompareEQ: ... == ... is true |
@@ -906,8 +928,49 @@ irGuardsEnsure
| test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:12:31:13 | Constant: - ... | == | test.cpp:31:7:31:7 | Load: x | 0 | 30 | 30 |
| test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:12:31:13 | Constant: - ... | == | test.cpp:31:7:31:7 | Load: x | 0 | 32 | 32 |
irGuardsEnsure_const
| test.c:7:9:7:13 | CompareGT: ... > ... | test.c:7:9:7:9 | Load: x | < | 1 | 11 | 11 |
| test.c:7:9:7:13 | CompareGT: ... > ... | test.c:7:9:7:9 | Load: x | >= | 1 | 8 | 8 |
| test.c:17:8:17:12 | CompareLT: ... < ... | test.c:17:8:17:8 | Load: x | < | 0 | 17 | 17 |
| test.c:17:8:17:12 | CompareLT: ... < ... | test.c:17:8:17:8 | Load: x | < | 0 | 18 | 18 |
| test.c:17:17:17:21 | CompareGT: ... > ... | test.c:17:17:17:17 | Load: y | >= | 2 | 18 | 18 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 2 | 2 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 31 | 31 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 34 | 34 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 35 | 35 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 39 | 39 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 42 | 42 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 43 | 43 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 45 | 45 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 46 | 46 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 52 | 52 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 56 | 56 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 58 | 58 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 59 | 59 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 62 | 62 |
| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | >= | 1 | 27 | 27 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | < | 10 | 35 | 35 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 2 | 2 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 39 | 39 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 42 | 42 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 43 | 43 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 45 | 45 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 46 | 46 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 52 | 52 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 56 | 56 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 58 | 58 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 59 | 59 |
| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 62 | 62 |
| test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:16 | Load: j | < | 10 | 43 | 43 |
| test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:16 | Load: j | < | 10 | 45 | 45 |
| test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:16 | Load: j | < | 10 | 46 | 46 |
| test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:16 | Load: j | < | 10 | 52 | 52 |
| test.c:44:12:44:16 | CompareGT: ... > ... | test.c:44:12:44:12 | Load: z | < | 1 | 52 | 52 |
| test.c:44:12:44:16 | CompareGT: ... > ... | test.c:44:12:44:12 | Load: z | >= | 1 | 45 | 45 |
| test.c:44:12:44:16 | CompareGT: ... > ... | test.c:44:12:44:12 | Load: z | >= | 1 | 46 | 46 |
| test.c:45:16:45:20 | CompareGT: ... > ... | test.c:45:16:45:16 | Load: y | >= | 1 | 46 | 46 |
| test.c:58:9:58:14 | CompareEQ: ... == ... | test.c:58:9:58:9 | Load: x | != | 0 | 58 | 58 |
| test.c:58:9:58:14 | CompareEQ: ... == ... | test.c:58:9:58:9 | Load: x | != | 0 | 62 | 62 |
| test.c:58:19:58:23 | CompareLT: ... < ... | test.c:58:19:58:19 | Load: y | >= | 0 | 62 | 62 |
| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:75:9:75:9 | Load: x | != | 0 | 79 | 79 |
| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:75:9:75:9 | Load: x | == | 0 | 76 | 76 |
| test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:85:8:85:8 | Load: x | == | 0 | 85 | 85 |
@@ -922,8 +985,15 @@ irGuardsEnsure_const
| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:11 | Load: x | == | 0 | 109 | 109 |
| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:11 | Load: x | == | 0 | 110 | 110 |
| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:11 | Load: x | == | 0 | 113 | 113 |
| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | < | 10 | 103 | 103 |
| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | >= | 10 | 70 | 70 |
| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | >= | 10 | 107 | 107 |
| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | >= | 10 | 109 | 109 |
| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | >= | 10 | 110 | 110 |
| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | >= | 10 | 113 | 113 |
| test.c:109:9:109:14 | CompareEQ: ... == ... | test.c:109:9:109:9 | Load: x | != | 0 | 109 | 109 |
| test.c:109:9:109:14 | CompareEQ: ... == ... | test.c:109:9:109:9 | Load: x | != | 0 | 113 | 113 |
| test.c:109:19:109:23 | CompareLT: ... < ... | test.c:109:19:109:19 | Load: y | >= | 0 | 113 | 113 |
| test.c:175:13:175:32 | CompareEQ: ... == ... | test.c:175:13:175:15 | Call: call to foo | != | 0 | 175 | 175 |
| test.c:175:13:175:32 | CompareEQ: ... == ... | test.c:175:13:175:15 | Call: call to foo | == | 0 | 175 | 175 |
| test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:7:31:7 | Load: x | != | -1 | 34 | 34 |

8
cpp/ql/test/library-tests/controlflow/guards-ir/tests.ql
View File

@@ -96,6 +96,10 @@ query predicate irGuardsCompare(int startLine, string msg) {
)
or
exists(AbstractValue value |
guard.comparesLt(left, k, true, value) and op = " < "
or
guard.comparesLt(left, k, false, value) and op = " >= "
or
guard.comparesEq(left, k, true, value) and op = " == "
or
guard.comparesEq(left, k, false, value) and op = " != "
@@ -138,6 +142,10 @@ query predicate irGuardsEnsure_const(
IRGuardCondition guard, Instruction left, string op, int k, int start, int end
) {
exists(IRBlock block, Operand leftOp |
guard.ensuresLt(leftOp, k, block, true) and op = "<"
or
guard.ensuresLt(leftOp, k, block, false) and op = ">="
or
guard.ensuresEq(leftOp, k, block, true) and op = "=="
or
guard.ensuresEq(leftOp, k, block, false) and op = "!="

30
cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected
View File

@@ -1,23 +1,33 @@
| 7 | 0 < x+0 when ... > ... is true |
| 7 | 0 >= x+0 when ... > ... is false |
| 7 | x < 0+1 when ... > ... is false |
| 7 | x < 1 when ... > ... is false |
| 7 | x >= 0+1 when ... > ... is true |
| 7 | x >= 1 when ... > ... is true |
| 17 | 0 < x+1 when ... < ... is false |
| 17 | 0 >= x+1 when ... && ... is true |
| 17 | 0 >= x+1 when ... < ... is true |
| 17 | 1 < y+0 when ... && ... is true |
| 17 | 1 < y+0 when ... > ... is true |
| 17 | 1 >= y+0 when ... > ... is false |
| 17 | x < 0 when ... && ... is true |
| 17 | x < 0 when ... < ... is true |
| 17 | x < 0+0 when ... && ... is true |
| 17 | x < 0+0 when ... < ... is true |
| 17 | x >= 0 when ... < ... is false |
| 17 | x >= 0+0 when ... < ... is false |
| 17 | y < 1+1 when ... > ... is false |
| 17 | y < 2 when ... > ... is false |
| 17 | y >= 1+1 when ... && ... is true |
| 17 | y >= 1+1 when ... > ... is true |
| 17 | y >= 2 when ... && ... is true |
| 17 | y >= 2 when ... > ... is true |
| 26 | 0 < x+0 when ... > ... is true |
| 26 | 0 >= x+0 when ... > ... is false |
| 26 | x < 0+1 when ... > ... is false |
| 26 | x < 1 when ... > ... is false |
| 26 | x >= 0+1 when ... > ... is true |
| 26 | x >= 1 when ... > ... is true |
| 31 | - ... != x+0 when ... == ... is false |
| 31 | - ... == x+0 when ... == ... is true |
| 31 | x != -1 when ... == ... is false |
@@ -26,20 +36,28 @@
| 31 | x == - ...+0 when ... == ... is true |
| 34 | 10 < j+1 when ... < ... is false |
| 34 | 10 >= j+1 when ... < ... is true |
| 34 | j < 10 when ... < ... is true |
| 34 | j < 10+0 when ... < ... is true |
| 34 | j >= 10 when ... < ... is false |
| 34 | j >= 10+0 when ... < ... is false |
| 42 | 10 < j+1 when ... < ... is false |
| 42 | 10 >= j+1 when ... < ... is true |
| 42 | j < 10 when ... < ... is true |
| 42 | j < 10+0 when ... < ... is true |
| 42 | j >= 10 when ... < ... is false |
| 42 | j >= 10+0 when ... < ... is false |
| 44 | 0 < z+0 when ... > ... is true |
| 44 | 0 >= z+0 when ... > ... is false |
| 44 | z < 0+1 when ... > ... is false |
| 44 | z < 1 when ... > ... is false |
| 44 | z >= 0+1 when ... > ... is true |
| 44 | z >= 1 when ... > ... is true |
| 45 | 0 < y+0 when ... > ... is true |
| 45 | 0 >= y+0 when ... > ... is false |
| 45 | y < 0+1 when ... > ... is false |
| 45 | y < 1 when ... > ... is false |
| 45 | y >= 0+1 when ... > ... is true |
| 45 | y >= 1 when ... > ... is true |
| 58 | 0 != x+0 when ... == ... is false |
| 58 | 0 != x+0 when ... \|\| ... is false |
| 58 | 0 < y+1 when ... < ... is false |
@@ -52,12 +70,19 @@
| 58 | x != 0+0 when ... \|\| ... is false |
| 58 | x == 0 when ... == ... is true |
| 58 | x == 0+0 when ... == ... is true |
| 58 | y < 0 when ... < ... is true |
| 58 | y < 0+0 when ... < ... is true |
| 58 | y >= 0 when ... < ... is false |
| 58 | y >= 0 when ... \|\| ... is false |
| 58 | y >= 0+0 when ... < ... is false |
| 58 | y >= 0+0 when ... \|\| ... is false |
| 61 | i == 0 when i is Case[0] |
| 61 | i == 1 when i is Case[1] |
| 61 | i == 2 when i is Case[2] |
| 74 | i < 11 when i is Case[0..10] |
| 74 | i < 21 when i is Case[11..20] |
| 74 | i >= 0 when i is Case[0..10] |
| 74 | i >= 11 when i is Case[11..20] |
| 75 | 0 != x+0 when ... == ... is false |
| 75 | 0 == x+0 when ... == ... is true |
| 75 | x != 0 when ... == ... is false |
@@ -90,7 +115,9 @@
| 94 | x == 0+0 when ... != ... is false |
| 102 | 10 < j+1 when ... < ... is false |
| 102 | 10 >= j+1 when ... < ... is true |
| 102 | j < 10 when ... < ... is true |
| 102 | j < 10+0 when ... < ... is true |
| 102 | j >= 10 when ... < ... is false |
| 102 | j >= 10+0 when ... < ... is false |
| 109 | 0 != x+0 when ... == ... is false |
| 109 | 0 != x+0 when ... \|\| ... is false |
@@ -104,6 +131,9 @@
| 109 | x != 0+0 when ... \|\| ... is false |
| 109 | x == 0 when ... == ... is true |
| 109 | x == 0+0 when ... == ... is true |
| 109 | y < 0 when ... < ... is true |
| 109 | y < 0+0 when ... < ... is true |
| 109 | y >= 0 when ... < ... is false |
| 109 | y >= 0 when ... \|\| ... is false |
| 109 | y >= 0+0 when ... < ... is false |
| 109 | y >= 0+0 when ... \|\| ... is false |

4
cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.ql
View File

@@ -28,6 +28,10 @@ where
)
or
exists(AbstractValue value |
guard.comparesLt(left, k, true, value) and op = " < "
or
guard.comparesLt(left, k, false, value) and op = " >= "
or
guard.comparesEq(left, k, true, value) and op = " == "
or
guard.comparesEq(left, k, false, value) and op = " != "