btorsim: implement rol and ror

This is a simple implementation delegating to sll and srl and or-ing the
results together

Signed-off-by: Ferdinand Bachmann <[email protected]>

Author: Ferdi265

src/btorsim/btorsim.cpp

@@ -257,6 +257,8 @@ parse_model_line (Btor2Line *l)
     case BTOR2_TAG_redand:
     case BTOR2_TAG_redor:
     case BTOR2_TAG_redxor:
+    case BTOR2_TAG_rol:
+    case BTOR2_TAG_ror:
     case BTOR2_TAG_sdiv:
     case BTOR2_TAG_sext:
     case BTOR2_TAG_sgt:
@@ -284,8 +286,6 @@ parse_model_line (Btor2Line *l)
 
     case BTOR2_TAG_fair:
     case BTOR2_TAG_justice:
-    case BTOR2_TAG_rol:
-    case BTOR2_TAG_ror:
     case BTOR2_TAG_saddo:
     case BTOR2_TAG_sdivo:
     case BTOR2_TAG_smod:
@@ -554,6 +554,20 @@ simulate (int64_t id)
         assert (args[0].type == BtorSimState::Type::BITVEC);
         res.bv_state = btorsim_bv_redxor (args[0].bv_state);
         break;
+      case BTOR2_TAG_rol:
+        assert (l->nargs == 2);
+        assert (res.type == BtorSimState::Type::BITVEC);
+        assert (args[0].type == BtorSimState::Type::BITVEC);
+        assert (args[1].type == BtorSimState::Type::BITVEC);
+        res.bv_state = btorsim_bv_rol (args[0].bv_state, args[1].bv_state);
+        break;
+      case BTOR2_TAG_ror:
+        assert (l->nargs == 2);
+        assert (res.type == BtorSimState::Type::BITVEC);
+        assert (args[0].type == BtorSimState::Type::BITVEC);
+        assert (args[1].type == BtorSimState::Type::BITVEC);
+        res.bv_state = btorsim_bv_ror (args[0].bv_state, args[1].bv_state);
+        break;
       case BTOR2_TAG_slice:
         assert (l->nargs == 1);
         assert (res.type == BtorSimState::Type::BITVEC);

src/btorsim/btorsimbv.c

@@ -1753,6 +1753,38 @@ btorsim_bv_sra (const BtorSimBitVector *a, const BtorSimBitVector *b)
   return res;
 }
 
+BtorSimBitVector *
+btorsim_bv_rol (const BtorSimBitVector *a, const BtorSimBitVector *b) {
+  BtorSimBitVector *width = btorsim_bv_uint64_to_bv(a->width, a->width);
+  BtorSimBitVector *rev = btorsim_bv_sub(width, b);
+
+  BtorSimBitVector *sll_part = btorsim_bv_sll(a, b);
+  BtorSimBitVector *srl_part = btorsim_bv_srl(a, rev);
+  BtorSimBitVector *res = btorsim_bv_or(sll_part, srl_part);
+
+  btorsim_bv_free(width);
+  btorsim_bv_free(rev);
+  btorsim_bv_free(sll_part);
+  btorsim_bv_free(srl_part);
+  return res;
+}
+
+BtorSimBitVector *
+btorsim_bv_ror (const BtorSimBitVector *a, const BtorSimBitVector *b) {
+  BtorSimBitVector *width = btorsim_bv_uint64_to_bv(a->width, a->width);
+  BtorSimBitVector *rev = btorsim_bv_sub(width, b);
+
+  BtorSimBitVector *srl_part = btorsim_bv_srl(a, b);
+  BtorSimBitVector *sll_part = btorsim_bv_sll(a, rev);
+  BtorSimBitVector *res = btorsim_bv_or(srl_part, sll_part);
+
+  btorsim_bv_free(width);
+  btorsim_bv_free(rev);
+  btorsim_bv_free(srl_part);
+  btorsim_bv_free(sll_part);
+  return res;
+}
+
 BtorSimBitVector *
 btorsim_bv_mul (const BtorSimBitVector *a, const BtorSimBitVector *b)
 {

src/btorsim/btorsimbv.h

@@ -191,6 +191,12 @@ BtorSimBitVector *btorsim_bv_srl (const BtorSimBitVector *a,
 BtorSimBitVector *btorsim_bv_sra (const BtorSimBitVector *a,
                                   const BtorSimBitVector *b);
 
+BtorSimBitVector *btorsim_bv_rol (const BtorSimBitVector *a,
+                                  const BtorSimBitVector *b);
+
+BtorSimBitVector *btorsim_bv_ror (const BtorSimBitVector *a,
+                                  const BtorSimBitVector *b);
+
 BtorSimBitVector *btorsim_bv_mul (const BtorSimBitVector *a,
                                   const BtorSimBitVector *b);