From 1c70a42041c7a2e14b651298bd7dd1e6820e89c0 Mon Sep 17 00:00:00 2001 From: Nikita Kraiouchkine Date: Mon, 17 Apr 2023 18:19:52 +0200 Subject: [PATCH] Remove guardEnsuresEqUnordered and update tests GuardCondition::ensuresEq is sufficient. Update test-cases and expected results + removed a QL warning --- README.md | 2 +- exercises-tests/Exercise7/Exercise7.expected | 1 - exercises-tests/Exercise8/Exercise8.expected | 1 - exercises/Exercise10.ql | 13 +------------ exercises/Exercise11.ql | 13 +------------ exercises/Exercise12.ql | 13 +------------ exercises/Exercise2.ql | 11 ----------- exercises/Exercise4.ql | 11 ----------- exercises/Exercise5.ql | 13 +------------ exercises/Exercise7.ql | 16 ++-------------- exercises/Exercise8.ql | 16 ++-------------- exercises/Exercise9.ql | 13 +------------ solutions-tests/Exercise7/Exercise7.expected | 1 - solutions-tests/Exercise8/Exercise8.expected | 1 - solutions/Exercise10.ql | 13 +------------ solutions/Exercise11.ql | 13 +------------ solutions/Exercise12.ql | 13 +------------ solutions/Exercise2.ql | 13 +------------ solutions/Exercise4.ql | 13 +------------ solutions/Exercise5.ql | 13 +------------ solutions/Exercise7.ql | 16 ++-------------- solutions/Exercise8.ql | 16 ++-------------- solutions/Exercise9.ql | 13 +------------ 23 files changed, 21 insertions(+), 227 deletions(-) diff --git a/README.md b/README.md index 2738e54..aadf48c 100644 --- a/README.md +++ b/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. diff --git a/exercises-tests/Exercise7/Exercise7.expected b/exercises-tests/Exercise7/Exercise7.expected index 3bca430..6dc6ab2 100644 --- a/exercises-tests/Exercise7/Exercise7.expected +++ b/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 | ... == ... | diff --git a/exercises-tests/Exercise8/Exercise8.expected b/exercises-tests/Exercise8/Exercise8.expected index 5e9a220..4808bd9 100644 --- a/exercises-tests/Exercise8/Exercise8.expected +++ b/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 | diff --git a/exercises/Exercise10.ql b/exercises/Exercise10.ql index 7b47bab..140fed7 100644 --- a/exercises/Exercise10.ql +++ b/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) ) } diff --git a/exercises/Exercise11.ql b/exercises/Exercise11.ql index 252673f..2e48b6b 100644 --- a/exercises/Exercise11.ql +++ b/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) ) } diff --git a/exercises/Exercise12.ql b/exercises/Exercise12.ql index eb84d65..fd62c8d 100644 --- a/exercises/Exercise12.ql +++ b/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) ) } diff --git a/exercises/Exercise2.ql b/exercises/Exercise2.ql index 9245637..f49b1d7 100644 --- a/exercises/Exercise2.ql +++ b/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`. diff --git a/exercises/Exercise4.ql b/exercises/Exercise4.ql index 316b6b5..faad749 100644 --- a/exercises/Exercise4.ql +++ b/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`. diff --git a/exercises/Exercise5.ql b/exercises/Exercise5.ql index 0ad9739..0413563 100644 --- a/exercises/Exercise5.ql +++ b/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) ) } diff --git a/exercises/Exercise7.ql b/exercises/Exercise7.ql index 1e05552..83af6ca 100644 --- a/exercises/Exercise7.ql +++ b/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) } } diff --git a/exercises/Exercise8.ql b/exercises/Exercise8.ql index a9a49dd..62fcef5 100644 --- a/exercises/Exercise8.ql +++ b/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) } } diff --git a/exercises/Exercise9.ql b/exercises/Exercise9.ql index 23aea50..e208a27 100644 --- a/exercises/Exercise9.ql +++ b/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) ) } diff --git a/solutions-tests/Exercise7/Exercise7.expected b/solutions-tests/Exercise7/Exercise7.expected index 3bca430..6dc6ab2 100644 --- a/solutions-tests/Exercise7/Exercise7.expected +++ b/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 | ... == ... | diff --git a/solutions-tests/Exercise8/Exercise8.expected b/solutions-tests/Exercise8/Exercise8.expected index 5e9a220..4808bd9 100644 --- a/solutions-tests/Exercise8/Exercise8.expected +++ b/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 | diff --git a/solutions/Exercise10.ql b/solutions/Exercise10.ql index 91bbd9b..30fb0dc 100644 --- a/solutions/Exercise10.ql +++ b/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) ) } diff --git a/solutions/Exercise11.ql b/solutions/Exercise11.ql index 252673f..2e48b6b 100644 --- a/solutions/Exercise11.ql +++ b/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) ) } diff --git a/solutions/Exercise12.ql b/solutions/Exercise12.ql index ca780b2..774dc97 100644 --- a/solutions/Exercise12.ql +++ b/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) ) } diff --git a/solutions/Exercise2.ql b/solutions/Exercise2.ql index d832da0..fef4b41 100644 --- a/solutions/Exercise2.ql +++ b/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) ) } diff --git a/solutions/Exercise4.ql b/solutions/Exercise4.ql index 1763035..6bf7b67 100644 --- a/solutions/Exercise4.ql +++ b/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) ) } diff --git a/solutions/Exercise5.ql b/solutions/Exercise5.ql index 8fee171..daa59b9 100644 --- a/solutions/Exercise5.ql +++ b/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) ) } diff --git a/solutions/Exercise7.ql b/solutions/Exercise7.ql index c528fef..71ea930 100644 --- a/solutions/Exercise7.ql +++ b/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) } } diff --git a/solutions/Exercise8.ql b/solutions/Exercise8.ql index 9d37910..4a97a15 100644 --- a/solutions/Exercise8.ql +++ b/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) } } diff --git a/solutions/Exercise9.ql b/solutions/Exercise9.ql index 23f398c..29e7938 100644 --- a/solutions/Exercise9.ql +++ b/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) ) }