Unbounded rotate for SMT-LIB2

Author: BrunoDutertre

src/api/yices_api.c

@@ -7334,6 +7334,37 @@ bool yices_check_bitshift(bvlogic_buffer_t *b, int32_t s) {
 }
 
 
+/*
+ * Check whether s is a valid shift amount for rotate_left/rotate_right in SMT-LIB2
+ * - SMT allows rotate by arbitrary amounts: ((_ rotate_left k) t) is the same
+ *   as ((_ rotate_left (k % n) t)) where n = number of bits in t.
+ *
+ * This function
+ * - return true if 0 <= s and store the normalize shift (s % b->nbits) in *s
+ * - otherwise set the error report and return false.
+ */
+bool yices_check_smt2_rotate(bvlogic_buffer_t *b, int32_t *s) {
+  int32_t shift;
+  uint32_t n;
+
+  shift = *s;
+  if (shift < 0) {
+    error_report_t *error = get_yices_error();
+    error->code = INVALID_BITSHIFT;
+    error->badval = shift;
+    return false;
+  }
+
+  n = bvlogic_buffer_bitsize(b);
+  if (shift >= n && n > 0) {
+    shift = shift % n;
+    *s = shift;
+  }
+
+  return true;
+}
+
+
 /*
  * Check whether [i, j] is a valid segment for a vector of n bits
  * - return true if 0 <= i <= j <= n

src/api/yices_extensions.h

@@ -423,6 +423,18 @@ extern bool yices_check_bvmul_buffer(bvarith_buffer_t *b1, bvarith_buffer_t *b2)
 extern bool yices_check_bitshift(bvlogic_buffer_t *b, int32_t s);
 
 
+/*
+ * Check whether s is a valid shift amount for rotate_left/rotate_right in SMT-LIB2
+ * - SMT allows rotate by arbitrary amounts: ((_ rotate_left k) t) is the same
+ *   as ((_ rotate_left (k % n) t)) where n = number of bits in t.
+ *
+ * This function
+ * - return true if 0 <= s and store the normalize shift (s % b->nbits) in *s
+ * - otherwise set the error report and return false.
+ */
+extern bool yices_check_smt2_rotate(bvlogic_buffer_t *b, int32_t *s) ;
+
+
 /*
  * Check whether [i, j] is a valid segment for a bitvector of size n
  * - return true if 0 <= i <= j < n

src/frontend/smt2/smt2_term_stack.c

@@ -216,13 +216,12 @@ static void eval_smt2_mk_bv_rotate_left(tstack_t *stack, stack_elem_t *f, uint32
   index = get_integer(stack, f);
   b = tstack_get_bvlbuffer(stack);
   bvl_set_elem(stack, b, f+1);
-  if (! yices_check_bitshift(b, index)) {
+  if (! yices_check_smt2_rotate(b, &index)) {
     report_yices_error(stack);
   }
   // we known 0 <= index <= bitsize of b
-  if (index < bvlogic_buffer_bitsize(b)) {
-    bvlogic_buffer_rotate_left(b, index);
-  }
+  bvlogic_buffer_rotate_left(b, index);
+
   tstack_pop_frame(stack);
   set_bvlogic_result(stack, b);
 }
@@ -245,13 +244,12 @@ static void eval_smt2_mk_bv_rotate_right(tstack_t *stack, stack_elem_t *f, uint3
   index = get_integer(stack, f);
   b = tstack_get_bvlbuffer(stack);
   bvl_set_elem(stack, b, f+1);
-  if (! yices_check_bitshift(b, index)) {
+  if (! yices_check_smt2_rotate(b, &index)) {
     report_yices_error(stack);
   }
-  // we known 0 <= index <= bitsize of b
-  if (index < bvlogic_buffer_bitsize(b)) {
-    bvlogic_buffer_rotate_right(b, index);
-  }
+  // we known 0 <= index < bitsize of b
+  bvlogic_buffer_rotate_right(b, index);
+
   tstack_pop_frame(stack);
   set_bvlogic_result(stack, b);
 }