summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-06-07 18:15:05 +0100
committerAlasdair Armstrong2018-06-07 18:15:38 +0100
commit6eaf3159474aa62b9afee843b0983dcfb23a4157 (patch)
treecfd7fe7c1cb65794ee9f17d058eec8c063d5f5cf
parent45554f2893667d951e39c8049631a986c1683857 (diff)
Fix bug in add_bits optimization
-rw-r--r--lib/sail.h2
-rw-r--r--src/c_backend.ml8
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))