step 8a: Find /some/ problematic accesses by reverting to simple var+…

…const checks

session-tests/example8a/example8a.expected

@@ -1,12 +1,9 @@
-| test.c:16:17:16:22 | call to malloc | test.c:16:24:16:27 | size | 0 | test.c:19:5:19:17 | access to array | test.c:19:9:19:12 | size | -1 | test.c:15:19:15:22 | size | test.c:15:19:15:22 | size |
-| test.c:16:17:16:22 | call to malloc | test.c:16:24:16:27 | size | 0 | test.c:21:5:21:13 | access to array | test.c:21:9:21:12 | size | 0 | test.c:15:19:15:22 | size | test.c:15:19:15:22 | size |
-| test.c:28:17:28:22 | call to malloc | test.c:28:24:28:27 | size | 0 | test.c:37:5:37:17 | access to array | test.c:37:9:37:12 | size | -1 | test.c:26:19:26:22 | size | test.c:26:19:26:22 | size |
-| test.c:28:17:28:22 | call to malloc | test.c:28:24:28:27 | size | 0 | test.c:39:5:39:13 | access to array | test.c:39:9:39:12 | size | 0 | test.c:26:19:26:22 | size | test.c:26:19:26:22 | size |
-| test.c:28:17:28:22 | call to malloc | test.c:28:24:28:27 | size | 0 | test.c:43:9:43:17 | access to array | test.c:43:13:43:16 | size | 0 | test.c:26:19:26:22 | size | test.c:26:19:26:22 | size |
-| test.c:28:17:28:22 | call to malloc | test.c:28:24:28:27 | size | 0 | test.c:44:9:44:21 | access to array | test.c:44:13:44:16 | size | 1 | test.c:26:19:26:22 | size | test.c:26:19:26:22 | size |
-| test.c:28:17:28:22 | call to malloc | test.c:28:24:28:27 | size | 0 | test.c:45:9:45:21 | access to array | test.c:45:13:45:16 | size | 2 | test.c:26:19:26:22 | size | test.c:26:19:26:22 | size |
-| test.c:63:17:63:22 | call to malloc | test.c:63:24:63:33 | alloc_size | 0 | test.c:68:5:68:23 | access to array | test.c:68:9:68:18 | alloc_size | -1 | test.c:51:19:51:28 | alloc_size | test.c:51:19:51:28 | alloc_size |
-| test.c:63:17:63:22 | call to malloc | test.c:63:24:63:33 | alloc_size | 0 | test.c:69:5:69:19 | access to array | test.c:69:9:69:18 | alloc_size | 0 | test.c:51:19:51:28 | alloc_size | test.c:51:19:51:28 | alloc_size |
-| test.c:63:17:63:22 | call to malloc | test.c:63:24:63:33 | alloc_size | 0 | test.c:73:9:73:23 | access to array | test.c:73:13:73:22 | alloc_size | 0 | test.c:51:19:51:28 | alloc_size | test.c:51:19:51:28 | alloc_size |
-| test.c:63:17:63:22 | call to malloc | test.c:63:24:63:33 | alloc_size | 0 | test.c:74:9:74:27 | access to array | test.c:74:13:74:22 | alloc_size | 1 | test.c:51:19:51:28 | alloc_size | test.c:51:19:51:28 | alloc_size |
-| test.c:63:17:63:22 | call to malloc | test.c:63:24:63:33 | alloc_size | 0 | test.c:75:9:75:27 | access to array | test.c:75:13:75:22 | alloc_size | 2 | test.c:51:19:51:28 | alloc_size | test.c:51:19:51:28 | alloc_size |
+| test.c:16:17:16:22 | call to malloc | test.c:16:24:16:27 | size | test.c:21:5:21:13 | access to array | test.c:21:9:21:12 | size | test.c:15:19:15:22 | size | 0 | test.c:15:19:15:22 | size | 0 |
+| test.c:28:17:28:22 | call to malloc | test.c:28:24:28:27 | size | test.c:39:5:39:13 | access to array | test.c:39:9:39:12 | size | test.c:26:19:26:22 | size | 0 | test.c:26:19:26:22 | size | 0 |
+| test.c:28:17:28:22 | call to malloc | test.c:28:24:28:27 | size | test.c:43:9:43:17 | access to array | test.c:43:13:43:16 | size | test.c:26:19:26:22 | size | 0 | test.c:26:19:26:22 | size | 0 |
+| test.c:28:17:28:22 | call to malloc | test.c:28:24:28:27 | size | test.c:44:9:44:21 | access to array | test.c:44:13:44:16 | size | test.c:26:19:26:22 | size | 0 | test.c:26:19:26:22 | size | 1 |
+| test.c:28:17:28:22 | call to malloc | test.c:28:24:28:27 | size | test.c:45:9:45:21 | access to array | test.c:45:13:45:16 | size | test.c:26:19:26:22 | size | 0 | test.c:26:19:26:22 | size | 2 |
+| test.c:63:17:63:22 | call to malloc | test.c:63:24:63:33 | alloc_size | test.c:69:5:69:19 | access to array | test.c:69:9:69:18 | alloc_size | test.c:51:19:51:28 | alloc_size | 0 | test.c:51:19:51:28 | alloc_size | 0 |
+| test.c:63:17:63:22 | call to malloc | test.c:63:24:63:33 | alloc_size | test.c:73:9:73:23 | access to array | test.c:73:13:73:22 | alloc_size | test.c:51:19:51:28 | alloc_size | 0 | test.c:51:19:51:28 | alloc_size | 0 |
+| test.c:63:17:63:22 | call to malloc | test.c:63:24:63:33 | alloc_size | test.c:74:9:74:27 | access to array | test.c:74:13:74:22 | alloc_size | test.c:51:19:51:28 | alloc_size | 0 | test.c:51:19:51:28 | alloc_size | 1 |
+| test.c:63:17:63:22 | call to malloc | test.c:63:24:63:33 | alloc_size | test.c:75:9:75:27 | access to array | test.c:75:13:75:22 | alloc_size | test.c:51:19:51:28 | alloc_size | 0 | test.c:51:19:51:28 | alloc_size | 2 |

session/example8a.ql

@@ -29,16 +29,20 @@ where
   // Same initializer variable
   bufferBase.(VariableAccess).getTarget() = bufInit and
   accessBase.(VariableAccess).getTarget() = accessInit and
-  bufInit = accessInit
-// +++
-// Identify questionable differences
-select buffer, bufferBase, bufferOffset, access, accessBase, accessOffset, bufInit, accessInit
+  bufInit = accessInit and
+  // +++
+  // Identify questionable differences
+  accessOffset >= bufferOffset
+select buffer, bufferBase, access, accessBase, bufInit, bufferOffset, accessInit, accessOffset
 
 /**
  * Extract base and offset from y = base+offset and y = base-offset.  For others, get y and 0.
  *
  * For cases like
  *     buf[alloc_size + 1];
+ *         ^^^^^^^^^^^^^^ expr
+ *         ^^^^^^^^^^ base
+ *                    ^^^ offset
  *
  * The more general
  *     buf[sz * x * y - 1];

session/session.org

@@ -446,19 +446,6 @@ To address these, take the query from the previous exercise and
    - This only handles very specific cases.  Constructing counterexamples is easy.
    - We will address this in the next section.
 
-*** TODO incoporate
-    #+BEGIN_SRC java
-      predicate isOffsetOutOfBoundsConstant(
-        ArrayExpr access, FunctionCall source, int allocSize, int accessOffset
-      ) {
-        ensureSameFunction(access, source) and
-        // allocatedBufferArrayAccess(access, source) and
-        allocSize = getMaxStatedValue(source.getArgument(0)) and
-        accessOffset = getFixedArrayOffset(access) and
-        accessOffset >= allocSize
-      }
-    #+END_SRC
-
 *** Solution:
     #+INCLUDE: "example8.ql" src java
 
@@ -482,9 +469,25 @@ To address these, take the query from the previous exercise and
    constants that flow to a given expression.  Another approach is global value
    numbering, used next.
 
+** Step 8a
+   Find problematic accesses by reverting to some /simple/ =var+const= checks using
+   =accessOffset= and =bufferOffset=.
+
+   Note:
+   - These will flag some false positives.
+   - The product expression =sz * x * y= is not easily checked for equality. 
+   These are addressed in the next step.
+
+*** Solution:
+    #+INCLUDE: "example8a.ql" src java
+
+*** First 5 results
+    #+INCLUDE: "../session-tests/example8a/example8a.expected" :lines "-6"’
+
 ** Step 9 -- Global Value Numbering
-   Range analyis won't bound =sz * x * y=, so switch to global value
-   numbering.
+   Range analyis won't bound =sz * x * y=, and simpl equality checks don't work at
+   the structure level, so switch to global value numbering.
+
    This is the case in the last test case, 
    #+begin_example
    void test_gvn_var(unsigned long x, unsigned long y, unsigned long sz)
@@ -524,15 +527,6 @@ To address these, take the query from the previous exercise and
    #+end_example
    we have to "evaluate" the expressions -- or at least bound them.
 
-*** DONE incorporate
-    Done by =ensureSameFunction= instead.
-    #+BEGIN_SRC java
-      predicate allocatedBufferArrayAccess(ArrayExpr access, FunctionCall alloc) {
-        alloc.getTarget().hasName("malloc") and
-        DataFlow::localExprFlow(alloc, access.getArrayBase())
-      }
-    #+END_SRC
-
 *** TODO incoporate
     #+BEGIN_SRC java
       int getFixedArrayOffset(ArrayExpr access) {