Skip to content

Commit 95c6f2f

Browse files
elazargelazarg
committed
gsl::narrow in ebpf_domain.cpp
Also: introduce num_safety.hpp and two helpers: to_signed() and to_unsigned() Signed-off-by: Elazar Gershuni <elazarg@gmail.com>
1 parent 2f6a368 commit 95c6f2f

4 files changed

Lines changed: 54 additions & 40 deletions

File tree

‎src/crab/array_domain.cpp‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
#include "config.hpp"
1616
#include "crab/array_domain.hpp"
1717
#include "crab/dsl_syntax.hpp"
18+
#include "crab_utils/num_safety.hpp"
1819
#include "spec_type_descriptors.hpp"
1920

2021
namespace crab::domains {
@@ -109,7 +110,8 @@ class cell_t final {
109110
cell_t(const offset_t offset, const unsigned size) : _offset(offset), _size(size) {}
110111

111112
static interval_t to_interval(const offset_t o, const unsigned size) {
112-
return {gsl::narrow<int>(o), number_t{gsl::narrow<int>(o)} + size - 1};
113+
const number_t lb{gsl::narrow<int>(o)};
114+
return {lb, lb + size - 1};
113115
}
114116

115117
public:
@@ -646,7 +648,7 @@ std::optional<linear_expression_t> array_domain_t::load(const NumAbsDomain& inv,
646648
}
647649
}
648650
offset_t o(k);
649-
unsigned size = gsl::narrow<unsigned>(width);
651+
unsigned size = to_unsigned(width);
650652
if (auto cell = lookup_array_map(kind).get_cell(o, size)) {
651653
return cell->get_scalar(kind);
652654
}
@@ -705,7 +707,7 @@ std::optional<linear_expression_t> array_domain_t::load(const NumAbsDomain& inv,
705707
} else {
706708
b = boost::endian::native_to_little<index_t>(b);
707709
}
708-
return kind == data_kind_t::uvalues ? number_t(b) : number_t(gsl::narrow_cast<int64_t>(b));
710+
return kind == data_kind_t::uvalues ? number_t(b) : number_t(to_signed(b));
709711
}
710712
}
711713
}

‎src/crab/ebpf_domain.cpp‎

Lines changed: 23 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -10,27 +10,19 @@
1010

1111
#include "boost/endian/conversion.hpp"
1212

13-
#include "crab/array_domain.hpp"
14-
#include "crab/ebpf_domain.hpp"
15-
1613
#include "asm_ostream.hpp"
1714
#include "asm_unmarshal.hpp"
1815
#include "config.hpp"
16+
#include "crab/array_domain.hpp"
17+
#include "crab/ebpf_domain.hpp"
18+
#include "crab_utils/num_safety.hpp"
1919
#include "dsl_syntax.hpp"
2020
#include "platform.hpp"
2121
#include "string_constraints.hpp"
2222

2323
using crab::domains::NumAbsDomain;
2424
namespace crab {
2525

26-
static auto to_signed(std::unsigned_integral auto x) -> std::make_signed_t<decltype(x)> {
27-
return static_cast<std::make_signed_t<decltype(x)>>(x);
28-
}
29-
30-
static auto to_unsigned(std::signed_integral auto x) -> std::make_unsigned_t<decltype(x)> {
31-
return static_cast<std::make_unsigned_t<decltype(x)>>(x);
32-
}
33-
3426
constexpr int MAX_PACKET_SIZE = 0xffff;
3527

3628
// Pointers in the BPF VM are defined to be 64 bits. Some contexts, like
@@ -80,7 +72,7 @@ static std::vector<linear_constraint_t> assume_bit_cst_interval(const NumAbsDoma
8072
}
8173
uint64_t src_int_value = src_n.value().cast_to<uint64_t>();
8274
if (!is64) {
83-
src_int_value = static_cast<uint32_t>(src_int_value);
75+
src_int_value = gsl::narrow_cast<uint32_t>(src_int_value);
8476
}
8577

8678
bool result;
@@ -1655,7 +1647,7 @@ static std::tuple<linear_expression_t, linear_expression_t> lb_ub_access_pair(co
16551647
void ebpf_domain_t::operator()(const ValidAccess& s) {
16561648
using namespace crab::dsl_syntax;
16571649

1658-
const bool is_comparison_check = s.width == static_cast<Value>(Imm{0});
1650+
const bool is_comparison_check = s.width == Value{Imm{0}};
16591651

16601652
const auto reg = reg_pack(s.reg);
16611653
// join_over_types instead of simple iteration is only needed for assume-assert
@@ -1679,7 +1671,7 @@ void ebpf_domain_t::operator()(const ValidAccess& s) {
16791671
if (s.offset < 0) {
16801672
require(inv, linear_constraint_t::false_const(), "Stack content is not numeric");
16811673
} else if (const auto pimm = std::get_if<Imm>(&s.width)) {
1682-
if (!inv.entail(static_cast<int>(pimm->v) <= reg.stack_numeric_size - s.offset)) {
1674+
if (!inv.entail(gsl::narrow<int>(pimm->v) <= reg.stack_numeric_size - s.offset)) {
16831675
require(inv, linear_constraint_t::false_const(), "Stack content is not numeric");
16841676
}
16851677
} else {
@@ -2023,8 +2015,8 @@ void ebpf_domain_t::operator()(const Mem& b) {
20232015
do_mem_store(b, *preg, data_reg.svalue, data_reg.uvalue, data_reg);
20242016
}
20252017
} else {
2026-
do_mem_store(b, number_t{T_NUM}, number_t{static_cast<int64_t>(std::get<Imm>(b.value).v)},
2027-
number_t{static_cast<uint64_t>(std::get<Imm>(b.value).v)}, {});
2018+
const uint64_t imm = std::get<Imm>(b.value).v;
2019+
do_mem_store(b, number_t{T_NUM}, number_t{to_signed(imm)}, number_t{imm}, {});
20282020
}
20292021
}
20302022

@@ -2187,7 +2179,7 @@ void ebpf_domain_t::operator()(const Call& call) {
21872179
if (const auto map_type = get_map_type(*maybe_fd_reg)) {
21882180
if (global_program_info->platform->get_map_type(*map_type).value_type == EbpfMapValueType::MAP) {
21892181
if (const auto inner_map_fd = get_map_inner_map_fd(*maybe_fd_reg)) {
2190-
do_load_mapfd(r0_reg, static_cast<int>(*inner_map_fd), true);
2182+
do_load_mapfd(r0_reg, to_signed(*inner_map_fd), true);
21912183
goto out;
21922184
}
21932185
} else {
@@ -2327,8 +2319,8 @@ void ebpf_domain_t::shl(const Reg& dst_reg, int imm, const int finite_width) {
23272319
const number_t ub = interval.ub().number().value();
23282320
uint64_t lb_n = lb.cast_to<uint64_t>();
23292321
uint64_t ub_n = ub.cast_to<uint64_t>();
2330-
const uint64_t uint_max = finite_width == 64 ? std::numeric_limits<uint64_t>::max()
2331-
: static_cast<uint64_t>(std::numeric_limits<uint32_t>::max());
2322+
const uint64_t uint_max = finite_width == 64 ? uint64_t{std::numeric_limits<uint64_t>::max()}
2323+
: uint64_t{std::numeric_limits<uint32_t>::max()};
23322324
if (lb_n >> (finite_width - imm) != ub_n >> (finite_width - imm)) {
23332325
// The bits that will be shifted out to the left are different,
23342326
// which means all combinations of remaining bits are possible.
@@ -2342,7 +2334,7 @@ void ebpf_domain_t::shl(const Reg& dst_reg, int imm, const int finite_width) {
23422334
ub_n = ub_n << imm & uint_max;
23432335
}
23442336
m_inv.set(dst.uvalue, interval_t{lb_n, ub_n});
2345-
if (static_cast<int64_t>(ub_n) >= static_cast<int64_t>(lb_n)) {
2337+
if (to_signed(ub_n) >= to_signed(lb_n)) {
23462338
m_inv.assign(dst.svalue, dst.uvalue);
23472339
} else {
23482340
havoc(dst.svalue);
@@ -2472,7 +2464,7 @@ void ebpf_domain_t::ashr(const Reg& dst_reg, const linear_expression_t& right_sv
24722464
}
24732465
}
24742466
m_inv.set(dst.svalue, interval_t{lb_n, ub_n});
2475-
if (static_cast<uint64_t>(ub_n) >= static_cast<uint64_t>(lb_n)) {
2467+
if (to_unsigned(ub_n) >= to_unsigned(lb_n)) {
24762468
m_inv.assign(dst.uvalue, dst.svalue);
24772469
} else {
24782470
havoc(dst.uvalue);
@@ -2500,10 +2492,10 @@ void ebpf_domain_t::operator()(const Bin& bin) {
25002492
int64_t imm;
25012493
if (bin.is64) {
25022494
// Use the full signed value.
2503-
imm = static_cast<int64_t>(pimm->v);
2495+
imm = to_signed(pimm->v);
25042496
} else {
25052497
// Use only the low 32 bits of the value.
2506-
imm = static_cast<int32_t>(pimm->v);
2498+
imm = gsl::narrow_cast<int32_t>(pimm->v);
25072499
bitwise_and(dst.svalue, dst.uvalue, std::numeric_limits<uint32_t>::max());
25082500
}
25092501
switch (bin.op) {
@@ -2521,13 +2513,13 @@ void ebpf_domain_t::operator()(const Bin& bin) {
25212513
if (imm == 0) {
25222514
return;
25232515
}
2524-
add(bin.dst, static_cast<int>(imm), finite_width);
2516+
add(bin.dst, gsl::narrow<int>(imm), finite_width);
25252517
break;
25262518
case Bin::Op::SUB:
25272519
if (imm == 0) {
25282520
return;
25292521
}
2530-
add(bin.dst, static_cast<int>(-imm), finite_width);
2522+
add(bin.dst, gsl::narrow<int>(-imm), finite_width);
25312523
break;
25322524
case Bin::Op::MUL:
25332525
mul(dst.svalue, dst.uvalue, imm, finite_width);
@@ -2556,7 +2548,7 @@ void ebpf_domain_t::operator()(const Bin& bin) {
25562548
case Bin::Op::AND:
25572549
// FIX: what to do with ptr&-8 as in counter/simple_loop_unrolled?
25582550
bitwise_and(dst.svalue, dst.uvalue, imm);
2559-
if (static_cast<int32_t>(imm) > 0) {
2551+
if (gsl::narrow<int32_t>(imm) > 0) {
25602552
// AND with immediate is only a 32-bit operation so svalue and uvalue are the same.
25612553
assume(dst.svalue <= imm);
25622554
assume(dst.uvalue <= imm);
@@ -2565,9 +2557,9 @@ void ebpf_domain_t::operator()(const Bin& bin) {
25652557
}
25662558
havoc_offsets(bin.dst);
25672559
break;
2568-
case Bin::Op::LSH: shl(bin.dst, static_cast<int32_t>(imm), finite_width); break;
2569-
case Bin::Op::RSH: lshr(bin.dst, static_cast<int32_t>(imm), finite_width); break;
2570-
case Bin::Op::ARSH: ashr(bin.dst, static_cast<int32_t>(imm), finite_width); break;
2560+
case Bin::Op::LSH: shl(bin.dst, gsl::narrow<int32_t>(imm), finite_width); break;
2561+
case Bin::Op::RSH: lshr(bin.dst, gsl::narrow<int32_t>(imm), finite_width); break;
2562+
case Bin::Op::ARSH: ashr(bin.dst, gsl::narrow<int32_t>(imm), finite_width); break;
25712563
case Bin::Op::XOR:
25722564
bitwise_xor(dst.svalue, dst.uvalue, imm);
25732565
havoc_offsets(bin.dst);
@@ -2728,7 +2720,7 @@ void ebpf_domain_t::operator()(const Bin& bin) {
27282720
// Use only the low 32 bits of the value.
27292721
bitwise_and(dst.svalue, dst.uvalue, std::numeric_limits<uint32_t>::max());
27302722
}
2731-
shl(bin.dst, static_cast<int32_t>(imm), finite_width);
2723+
shl(bin.dst, gsl::narrow_cast<int32_t>(imm), finite_width);
27322724
break;
27332725
}
27342726
}
@@ -2746,7 +2738,7 @@ void ebpf_domain_t::operator()(const Bin& bin) {
27462738
// Use only the low 32 bits of the value.
27472739
bitwise_and(dst.svalue, dst.uvalue, std::numeric_limits<uint32_t>::max());
27482740
}
2749-
lshr(bin.dst, static_cast<int32_t>(imm), finite_width);
2741+
lshr(bin.dst, gsl::narrow_cast<int32_t>(imm), finite_width);
27502742
break;
27512743
}
27522744
}

‎src/crab_utils/num_big.hpp‎

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -9,17 +9,12 @@
99

1010
#include <boost/multiprecision/cpp_int.hpp>
1111

12+
#include "crab_utils/num_safety.hpp"
1213
#include "debug.hpp"
1314
using boost::multiprecision::cpp_int;
1415

1516
namespace crab {
1617

17-
template <typename T>
18-
concept is_enum = std::is_enum_v<T>;
19-
20-
template <std::integral T>
21-
using swap_signedness = std::conditional_t<std::is_signed_v<T>, std::make_unsigned_t<T>, std::make_signed_t<T>>;
22-
2318
class number_t final {
2419
cpp_int _n{};
2520

‎src/crab_utils/num_safety.hpp‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
// Copyright (c) Prevail Verifier contributors.
2+
// SPDX-License-Identifier: MIT
3+
#pragma once
4+
5+
#include <concepts>
6+
7+
#include <gsl/narrow>
8+
9+
namespace crab {
10+
11+
template <typename T>
12+
concept is_enum = std::is_enum_v<T>;
13+
14+
template <std::integral T>
15+
using swap_signedness = std::conditional_t<std::is_signed_v<T>, std::make_unsigned_t<T>, std::make_signed_t<T>>;
16+
17+
static auto to_signed(std::unsigned_integral auto x) -> std::make_signed_t<decltype(x)> {
18+
return static_cast<std::make_signed_t<decltype(x)>>(x);
19+
}
20+
21+
static auto to_unsigned(std::signed_integral auto x) -> std::make_unsigned_t<decltype(x)> {
22+
return static_cast<std::make_unsigned_t<decltype(x)>>(x);
23+
}
24+
25+
} // namespace crab

0 commit comments

Comments
 (0)