Remove guardEnsuresEqUnordered and update tests

GuardCondition::ensuresEq is sufficient.
Update test-cases and expected results + removed a QL warning

README.md

@@ -110,7 +110,7 @@ Validation involves a comparison of the `input_types` parameter with a value ret
 There are three steps to this exercise:
 1. Find all calls to `DYN_INPUT_TYPE`.
 2. Restrict the set of `GuardCondition`s to those that have local data-flow from the result of a `DYN_INPUT_TYPE` call.
-3. Check if the `GuardCondition` ensures equality against the result of `DYN_INPUT_TYPE` and guards the basic block of the `input` access.
+3. Check if the `GuardCondition` ensures equality against the result of `DYN_INPUT_TYPE` and guards the basic block of the `input` access. Use `GuardCondition::ensuresEq` to model that equality comparison.
 
 Complete the `typeValidationGuard` predicate and output all `input` accesses that are not guarded by a type validation check.
 

exercises-tests/Exercise7/Exercise7.expected

@@ -1,4 +1,3 @@
-WARNING: Unused method getInputParameter (/Users/kraiouchkine/internal/codeql-workshop-dataflow-c/solutions/Exercise7.ql:84,13-30)
 | test.c:32:10:32:17 | access to array | test.c:53:14:54:24 | ... == ... |
 | test.c:32:10:32:17 | access to array | test.c:58:7:58:75 | ... != ... |
 | test.c:32:10:32:17 | access to array | test.c:71:7:71:76 | ... == ... |

exercises-tests/Exercise8/Exercise8.expected

@@ -1,4 +1,3 @@
-WARNING: Unused method getInputParameter (/Users/kraiouchkine/internal/codeql-workshop-dataflow-c/solutions/Exercise8.ql:107,13-30)
 | test.c:32:10:32:17 | access to array |
 | test.c:32:28:32:35 | access to array |
 | test.c:33:10:33:17 | access to array |

exercises/Exercise10.ql

@@ -58,17 +58,6 @@ class TypeValidationCall extends FunctionCall {
   }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -78,7 +67,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }

exercises/Exercise11.ql

@@ -53,17 +53,6 @@ class TypeValidationCall extends FunctionCall {
   }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -73,7 +62,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }

exercises/Exercise12.ql

@@ -53,17 +53,6 @@ class TypeValidationCall extends FunctionCall {
   }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -73,7 +62,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }

exercises/Exercise2.ql

@@ -22,17 +22,6 @@ class TypeValidationCall extends FunctionCall {
   }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.

exercises/Exercise4.ql

@@ -24,17 +24,6 @@ class TypeValidationCall extends FunctionCall {
   TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.

exercises/Exercise5.ql

@@ -24,17 +24,6 @@ class TypeValidationCall extends FunctionCall {
   TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -44,7 +33,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }

exercises/Exercise7.ql

@@ -24,17 +24,6 @@ class TypeValidationCall extends FunctionCall {
   TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -44,7 +33,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }
@@ -80,8 +69,7 @@ module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig {
 class EntrypointFunction extends Function {
   EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) }
 
-  Parameter getInputParameter() { result = this.getParameter(0) }
-
+  // Parameter getInputParameter() { result = this.getParameter(0) }
   Parameter getInputTypesParameter() { result = this.getParameter(1) }
 }
 

exercises/Exercise8.ql

@@ -37,17 +37,6 @@ class TypeValidationCall extends FunctionCall {
   }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -57,7 +46,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }
@@ -94,8 +83,7 @@ module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig {
 class EntrypointFunction extends Function {
   EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) }
 
-  Parameter getInputParameter() { result = this.getParameter(0) }
-
+  // Parameter getInputParameter() { result = this.getParameter(0) }
   Parameter getInputTypesParameter() { result = this.getParameter(1) }
 }
 

exercises/Exercise9.ql

@@ -53,17 +53,6 @@ class TypeValidationCall extends FunctionCall {
   }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -73,7 +62,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }

solutions-tests/Exercise7/Exercise7.expected

@@ -1,4 +1,3 @@
-WARNING: Unused method getInputParameter (/Users/kraiouchkine/internal/codeql-workshop-dataflow-c/solutions/Exercise7.ql:84,13-30)
 | test.c:32:10:32:17 | access to array | test.c:53:14:54:24 | ... == ... |
 | test.c:32:10:32:17 | access to array | test.c:58:7:58:75 | ... != ... |
 | test.c:32:10:32:17 | access to array | test.c:71:7:71:76 | ... == ... |

solutions-tests/Exercise8/Exercise8.expected

@@ -1,4 +1,3 @@
-WARNING: Unused method getInputParameter (/Users/kraiouchkine/internal/codeql-workshop-dataflow-c/solutions/Exercise8.ql:107,13-30)
 | test.c:32:10:32:17 | access to array |
 | test.c:32:28:32:35 | access to array |
 | test.c:33:10:33:17 | access to array |

solutions/Exercise10.ql

@@ -58,17 +58,6 @@ class TypeValidationCall extends FunctionCall {
   }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -78,7 +67,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }

solutions/Exercise11.ql

@@ -53,17 +53,6 @@ class TypeValidationCall extends FunctionCall {
   }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -73,7 +62,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }

solutions/Exercise12.ql

@@ -53,17 +53,6 @@ class TypeValidationCall extends FunctionCall {
   }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -73,7 +62,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }

solutions/Exercise2.ql

@@ -18,17 +18,6 @@ class TypeValidationCall extends FunctionCall {
   TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -38,7 +27,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true)
+    guard.ensuresEq(dest, other, 0, block, true)
   )
 }
 

solutions/Exercise4.ql

@@ -24,17 +24,6 @@ class TypeValidationCall extends FunctionCall {
   TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -44,7 +33,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }

solutions/Exercise5.ql

@@ -24,17 +24,6 @@ class TypeValidationCall extends FunctionCall {
   TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -44,7 +33,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }

solutions/Exercise7.ql

@@ -24,17 +24,6 @@ class TypeValidationCall extends FunctionCall {
   TypeValidationCall() { this.getTarget().hasName("DYN_INPUT_TYPE") }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -44,7 +33,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }
@@ -81,8 +70,7 @@ module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig {
 class EntrypointFunction extends Function {
   EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) }
 
-  Parameter getInputParameter() { result = this.getParameter(0) }
-
+  // Parameter getInputParameter() { result = this.getParameter(0) }
   Parameter getInputTypesParameter() { result = this.getParameter(1) }
 }
 

solutions/Exercise8.ql

@@ -47,17 +47,6 @@ class TypeValidationCall extends FunctionCall {
   }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -67,7 +56,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }
@@ -104,8 +93,7 @@ module InputTypesToTypeValidationConfig implements DataFlow::ConfigSig {
 class EntrypointFunction extends Function {
   EntrypointFunction() { this.hasName(["EP_copy_mem", "EP_print_val", "EP_write_val_to_mem"]) }
 
-  Parameter getInputParameter() { result = this.getParameter(0) }
-
+  // Parameter getInputParameter() { result = this.getParameter(0) }
   Parameter getInputTypesParameter() { result = this.getParameter(1) }
 }
 

solutions/Exercise9.ql

@@ -53,17 +53,6 @@ class TypeValidationCall extends FunctionCall {
   }
 }
 
-/**
- * Holds if `op1` and `op2` are checked for equality in any order
- * with no distinction between left and right operands of the equality check
- */
-predicate guardEnsuresEqUnordered(
-  Expr op1, Expr op2, GuardCondition guard, BasicBlock block, boolean areEqual
-) {
-  guard.ensuresEq(op1, op2, 0, block, areEqual) or
-  guard.ensuresEq(op2, op1, 0, block, areEqual)
-}
-
 /**
  * Relates a `call` to a `guard`, which uses the result of the call to validate
  * equality of the result of `call` against `other` to guard `block`.
@@ -73,7 +62,7 @@ predicate typeValidationGuard(
 ) {
   exists(Expr dest |
     DataFlow::localExprFlow(call, dest) and
-    guardEnsuresEqUnordered(dest, other, guard, block, true) and
+    guard.ensuresEq(dest, other, 0, block, true) and
     InputTypesToTypeValidation::hasFlowToExpr(other)
   )
 }