From 6eaf3159474aa62b9afee843b0983dcfb23a4157 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 7 Jun 2018 18:15:05 +0100 Subject: Fix bug in add_bits optimization --- lib/sail.h | 2 +- src/c_backend.ml | 8 ++------ 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/lib/sail.h b/lib/sail.h index 29a0c0f8..99b57d8a 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -466,7 +466,7 @@ void replicate_bits(bv_t *rop, const bv_t op1, const mpz_t op2) { uint64_t fast_replicate_bits(const uint64_t shift, const uint64_t v, const int64_t times) { uint64_t r = v; for (int i = 1; i < times; ++i) { - r |= v << shift; + r |= (r << shift); } return r; } diff --git a/src/c_backend.ml b/src/c_backend.ml index 59656152..f58093b0 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -977,13 +977,9 @@ let analyze_primop' ctx env l id args typ = | "eq_int", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> AE_val (AV_C_fragment (F_op (v1, "==", v2), typ)) - (* - | "add_int", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> - AE_val (AV_C_fragment (F_op (v1, "+", v2), typ)) - *) - + (* | "add_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> - AE_val (AV_C_fragment (F_op (v1, "+", v2), typ)) + AE_val (AV_C_fragment (F_op (v1, "+", v2), typ)) *) | "xor_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> AE_val (AV_C_fragment (F_op (v1, "^", v2), typ)) -- cgit v1.2.3