From 9d0df3b6a720b3d38dd8c9a4ab04e811f0dd1811 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Sat, 19 Oct 2024 09:43:34 -0700 Subject: [PATCH] Reject binary ops where the source is an uninitialized register (#740) Signed-off-by: Alan Jowett --- src/assertions.cpp | 27 ++- src/test/test_yaml.cpp | 1 + test-data/uninit.yaml | 497 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 513 insertions(+), 12 deletions(-) create mode 100644 test-data/uninit.yaml diff --git a/src/assertions.cpp b/src/assertions.cpp index 34a3d2212..6904c2a0f 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -192,17 +192,13 @@ class AssertExtractor { } vector operator()(const Atomic& ins) const { - vector res; - res.emplace_back(TypeConstraint{ins.access.basereg, TypeGroup::pointer}); - res.emplace_back( - ValidAccess{ins.access.basereg, ins.access.offset, Imm{static_cast(ins.access.width)}, false}); - if (ins.op == Atomic::Op::CMPXCHG) { - // The memory contents pointed to by ins.access will be compared - // against the value of the ins.valreg register. Only numbers are - // supported. - res.emplace_back(TypeConstraint{ins.valreg, TypeGroup::number}); - } - return res; + + return { + Assert{TypeConstraint{ins.valreg, TypeGroup::number}}, + Assert{TypeConstraint{ins.access.basereg, TypeGroup::pointer}}, + Assert{ValidAccess{ins.access.basereg, ins.access.offset, Imm{static_cast(ins.access.width)}, + false}}, + }; } vector operator()(const Un ins) const { return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}}; } @@ -246,7 +242,14 @@ class AssertExtractor { } return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}}; } - default: return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}}; + // For all other binary operations, the destination register must be a number and the source must either be an immediate or a number. + default: + if (const auto src = std::get_if(&ins.v)) { + return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}, + Assert{TypeConstraint{*src, TypeGroup::number}}}; + } else { + return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}}; + } } assert(false); } diff --git a/src/test/test_yaml.cpp b/src/test/test_yaml.cpp index 71975f2c6..ac8a0b9f5 100644 --- a/src/test/test_yaml.cpp +++ b/src/test/test_yaml.cpp @@ -39,5 +39,6 @@ YAML_CASE("test-data/sext.yaml") YAML_CASE("test-data/shift.yaml") YAML_CASE("test-data/stack.yaml") YAML_CASE("test-data/subtract.yaml") +YAML_CASE("test-data/uninit.yaml") YAML_CASE("test-data/unop.yaml") YAML_CASE("test-data/unsigned.yaml") diff --git a/test-data/uninit.yaml b/test-data/uninit.yaml new file mode 100644 index 000000000..397883f5d --- /dev/null +++ b/test-data/uninit.yaml @@ -0,0 +1,497 @@ +# Copyright (c) Prevail Verifier contributors. +# SPDX-License-Identifier: MIT +--- +test-case: addition of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 += r3 + +post: [] + +messages: + - "0: Invalid type (r3.type in {number, ctx, stack, packet, shared})" + - "CRAB ERROR: Cannot convert bottom to tuple" + +--- +test-case: subtraction of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 -= r3 + +post: [] + +messages: + - "0: Cannot subtract pointers to different regions (r3.type == number or r0.type == r3.type in {ctx, stack, packet})" + +--- +test-case: multiplication of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 *= r3 + +post: + - "r0.type=number" + +messages: + - "0: Invalid type (r3.type == number)" + +--- +test-case: division of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 /= r3 + +post: + - "r0.svalue=[0, 1]" + - "r0.svalue=r0.uvalue" + - "r0.type=number" + - "r0.uvalue=[0, 1]" + +messages: + - "0: Only numbers can be used as divisors (r3 != 0)" + +--- +test-case: signed division of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 s/= r3 + +post: + - "r0.svalue=[-1, 1]" + - "r0.type=number" + +messages: + - "0: Only numbers can be used as divisors (r3 != 0)" + +--- +test-case: modulo of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 %= r3 + +post: + - "r0.svalue=[0, 1]" + - "r0.svalue=r0.uvalue" + - "r0.type=number" + - "r0.uvalue=[0, 1]" + +messages: + - "0: Only numbers can be used as divisors (r3 != 0)" + +--- +test-case: signed modulo of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 s%= r3 + +post: + - "r0.svalue=[0, 1]" + - "r0.svalue=r0.uvalue" + - "r0.type=number" + - "r0.uvalue=[0, 1]" + +messages: + - "0: Only numbers can be used as divisors (r3 != 0)" + +--- +test-case: AND of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 &= r3 + +post: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +messages: + - "0: Invalid type (r3.type == number)" + +--- +test-case: OR of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 |= r3 + +post: + - "r0.type=number" + +messages: + - "0: Invalid type (r3.type == number)" + +--- +test-case: XOR of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 ^= r3 + +post: + - "r0.type=number" + +messages: + - "0: Invalid type (r3.type == number)" + +--- +test-case: LSH of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 <<= r3 + +post: + - "r0.type=number" + +messages: + - "0: Invalid type (r3.type == number)" + +--- +test-case: RSH of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 >>= r3 + +post: + - "r0.type=number" + +messages: + - "0: Invalid type (r3.type == number)" + +--- +test-case: ARSH of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 s>>= r3 + +post: + - "r0.type=number" + +messages: + - "0: Invalid type (r3.type == number)" + +--- +test-case: MOVSX8 of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 s8= r3 + +post: + - "r0.type=number" + +messages: + - "0: Invalid type (r3.type == number)" + +--- +test-case: MOVSX16 of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 s16= r3 + +post: + - "r0.type=number" + +messages: + - "0: Invalid type (r3.type == number)" + +--- +test-case: MOVSX32 of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 s32= r3 + +post: + - "r0.type=number" + +messages: + - "0: Invalid type (r3.type == number)" + +--- +test-case: MOV of a number and an uninitialized register + +pre: + - "r0.type=number" + - "r0.uvalue=1" + - "r0.svalue=1" + +code: + : | + r0 = r3 + +post: + - "r0.svalue=r3.svalue" + - "r0.type=r3.type" + - "r0.uvalue=r3.uvalue" + +--- +test-case: Store uninitialized register to context - 8 bytes + +pre: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +code: + : | + *(u64 *)(r1 + 0) = r0 + +post: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +messages: + - "0: Only numbers can be stored to externally-visible regions (r1.type != stack -> r0.type == number)" + +--- +test-case: Store uninitialized register to context - 4 bytes + +pre: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +code: + : | + *(u32 *)(r1 + 0) = r0 + +post: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +messages: + - "0: Invalid type (r0.type == number)" + +--- +test-case: Store uninitialized register to context - 2 bytes + +pre: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +code: + : | + *(u16 *)(r1 + 0) = r0 + +post: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +messages: + - "0: Invalid type (r0.type == number)" + +--- +test-case: Store uninitialized register to context - 1 bytes + +pre: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +code: + : | + *(u8 *)(r1 + 0) = r0 + +post: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +messages: + - "0: Invalid type (r0.type == number)" + +--- +test-case: Atomic add uninitialized register to context + +pre: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +code: + : | + lock *(u64 *)(r1 + 0) += r5 + +post: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +messages: + - "0: Invalid type (r5.type == number)" + +--- +test-case: Atomic AND uninitialized register to context + +pre: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +code: + : | + lock *(u64 *)(r1 + 0) &= r5 + +post: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +messages: + - "0: Invalid type (r5.type == number)" + +--- +test-case: Atomic OR uninitialized register to context + +pre: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +code: + : | + lock *(u64 *)(r1 + 0) |= r5 + +post: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +messages: + - "0: Invalid type (r5.type == number)" + +--- +test-case: Atomic XOR uninitialized register to context + +pre: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +code: + : | + lock *(u64 *)(r1 + 0) |= r5 + +post: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +messages: + - "0: Invalid type (r5.type == number)" + +--- +test-case: Atomic XHNG uninitialized register to context + +pre: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +code: + : | + lock *(u64 *)(r1 + 0) x= r5 + +post: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +messages: + - "0: Invalid type (r5.type == number)" + +--- +test-case: Atomic CMPXCHG uninitialized register to context + +pre: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +code: + : | + lock *(u64 *)(r1 + 0) x= r5 + +post: + - "r1.type=ctx" + - "r1.ctx_offset=0" + +messages: + - "0: Invalid type (r5.type == number)"