Skip to content

Commit 04eec15

Browse files
filipeomfilipeom
committed
Add indexed rotate operators
This is needed because some solvers may follow the SMT-LIB standard strictly and only implement the rotate operators using indicies. Closes #625 Closes #627 BREAKING: This change intentionally breaks the `rotate_{left,right}` operators to take an integer as the first argument. This is to force users to make a decision on whether to continue using the previous behavior with `ext_rotate_{left,right}` or start using the new API.
1 parent c44b865 commit 04eec15

19 files changed

Lines changed: 187 additions & 50 deletions

‎src/smtml/bitwuzla_mappings.default.ml‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -365,9 +365,17 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
365365

366366
let rem_u t1 t2 = mk_term2 Kind.Bv_urem t1 t2
367367

368-
let rotate_left t1 t2 = mk_term2 Kind.Bv_rol t1 t2
368+
let rotate_left n t =
369+
let bitwidth = Sort.bv_size (Term.sort t) in
370+
mk_term2 Kind.Bv_rol t (of_z (Z.of_int n) bitwidth)
369371

370-
let rotate_right t1 t2 = mk_term2 Kind.Bv_ror t1 t2
372+
let rotate_right n t =
373+
let bitwidth = Sort.bv_size (Term.sort t) in
374+
mk_term2 Kind.Bv_ror t (of_z (Z.of_int n) bitwidth)
375+
376+
let ext_rotate_left t1 t2 = mk_term2 Kind.Bv_rol t1 t2
377+
378+
let ext_rotate_right t1 t2 = mk_term2 Kind.Bv_ror t1 t2
371379

372380
let nego t = mk_term1 Kind.Bv_nego t
373381

‎src/smtml/cvc5_mappings.default.ml‎

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -305,11 +305,21 @@ module Fresh_cvc5 () = struct
305305

306306
let rem_u t1 t2 = Term.mk_term tm Kind.Bitvector_urem [| t1; t2 |]
307307

308-
let rotate_left t1 t2 =
309-
Term.mk_term tm Kind.Bitvector_rotate_left [| t1; t2 |]
308+
let rotate_left n t =
309+
let op = Op.mk_op tm Kind.Bitvector_rotate_left [| n |] in
310+
Term.mk_term_op tm op [| t |]
311+
312+
let rotate_right n t =
313+
let op = Op.mk_op tm Kind.Bitvector_rotate_right [| n |] in
314+
Term.mk_term_op tm op [| t |]
315+
316+
let ext_rotate_left _ _ =
317+
Fmt.failwith "%s:%d: %s not implemented. Use 'rotate_left' instead"
318+
__MODULE__ __LINE__ __FUNCTION__
310319

311-
let rotate_right t1 t2 =
312-
Term.mk_term tm Kind.Bitvector_rotate_right [| t1; t2 |]
320+
let ext_rotate_right _ _ =
321+
Fmt.failwith "%s:%d: %s not implemented. Use 'rotate_right' instead"
322+
__MODULE__ __LINE__ __FUNCTION__
313323

314324
let nego _ =
315325
Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__

‎src/smtml/dolmenexpr_to_expr.ml‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -338,9 +338,13 @@ module DolmenIntf = struct
338338

339339
let rem_u = DTerm.Bitv.urem
340340

341-
let rotate_left t1 t2 = DTerm.Bitv.rotate_left (int_of_term t2) t1
341+
let rotate_left n t = DTerm.Bitv.rotate_left n t
342342

343-
let rotate_right t1 t2 = DTerm.Bitv.rotate_right (int_of_term t2) t1
343+
let rotate_right n t = DTerm.Bitv.rotate_right n t
344+
345+
let ext_rotate_left t1 t2 = DTerm.Bitv.rotate_left (int_of_term t2) t1
346+
347+
let ext_rotate_right t1 t2 = DTerm.Bitv.rotate_right (int_of_term t2) t1
344348

345349
let nego _ =
346350
Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__

‎src/smtml/dolmenexpr_to_expr.mli‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -287,9 +287,13 @@ module DolmenIntf : sig
287287

288288
val rem_u : term -> term -> term
289289

290-
val rotate_left : term -> term -> term
290+
val rotate_left : int -> term -> term
291291

292-
val rotate_right : term -> term -> term
292+
val rotate_right : int -> term -> term
293+
294+
val ext_rotate_left : term -> term -> term
295+
296+
val ext_rotate_right : term -> term -> term
293297

294298
val nego : term -> term
295299

‎src/smtml/eval.ml‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -522,6 +522,12 @@ module Bitv = struct
522522
| Clz -> to_bitv (Bitvector.clz bv)
523523
| Ctz -> to_bitv (Bitvector.ctz bv)
524524
| Popcnt -> to_bitv (Bitvector.popcnt bv)
525+
| Rotl n ->
526+
let shift_count = Bitvector.make (Z.of_int n) (Bitvector.numbits bv) in
527+
to_bitv (Bitvector.rotate_left bv shift_count)
528+
| Rotr n ->
529+
let shift_count = Bitvector.make (Z.of_int n) (Bitvector.numbits bv) in
530+
to_bitv (Bitvector.rotate_right bv shift_count)
525531
| _ ->
526532
eval_error
527533
(`Unsupported_operator (`Unop op, Ty_bitv (Bitvector.numbits bv)))
@@ -543,8 +549,8 @@ module Bitv = struct
543549
| Shl -> to_bitv (Bitvector.shl bv1 bv2)
544550
| ShrL -> to_bitv (Bitvector.lshr bv1 bv2)
545551
| ShrA -> to_bitv (Bitvector.ashr bv1 bv2)
546-
| Rotl -> to_bitv (Bitvector.rotate_left bv1 bv2)
547-
| Rotr -> to_bitv (Bitvector.rotate_right bv1 bv2)
552+
| Ext_rotl -> to_bitv (Bitvector.rotate_left bv1 bv2)
553+
| Ext_rotr -> to_bitv (Bitvector.rotate_right bv1 bv2)
548554
| _ -> eval_error (`Unsupported_operator (`Binop op, Ty_bitv 0))
549555

550556
let[@inline] relop op bv1 bv2 =

‎src/smtml/feature.ml‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,8 @@ let of_unop (unop : Ty.Unop.t) : string =
3131
| Regexp_plus -> "Regexp_plus"
3232
| Regexp_opt -> "Regexp_opt"
3333
| Regexp_comp -> "Regexp_comp"
34+
| Rotl _ -> "Rotl"
35+
| Rotr _ -> "Rotr"
3436

3537
let of_binop (binop : Ty.Binop.t) : string =
3638
match binop with
@@ -52,8 +54,8 @@ let of_binop (binop : Ty.Binop.t) : string =
5254
| Min -> "Min"
5355
| Max -> "Max"
5456
| Copysign -> "Copysign"
55-
| Rotl -> "Rotl"
56-
| Rotr -> "Rotr"
57+
| Ext_rotl -> "Ext_rotl"
58+
| Ext_rotr -> "Ext_rotr"
5759
| At -> "At"
5860
| List_cons -> "List_cons"
5961
| List_append -> "List_append"
@@ -211,6 +213,8 @@ let ctor_names =
211213
; Regexp_plus
212214
; Regexp_opt
213215
; Regexp_comp
216+
; Rotl 0
217+
; Rotr 0
214218
]
215219
in
216220
let binops =
@@ -233,8 +237,8 @@ let ctor_names =
233237
; Min
234238
; Max
235239
; Copysign
236-
; Rotl
237-
; Rotr
240+
; Ext_rotl
241+
; Ext_rotr
238242
; At
239243
; List_cons
240244
; List_append (* String *)

‎src/smtml/mappings.ml‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -372,6 +372,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
372372
| Popcnt -> popcnt bitwidth t
373373
| Neg -> Bitv.neg t
374374
| Not -> Bitv.lognot t
375+
| Rotl n -> Bitv.rotate_left n t
376+
| Rotr n -> Bitv.rotate_right n t
375377
| op ->
376378
Fmt.failwith {|%s: Unsupported %s operator "%a"|} __MODULE__
377379
__FUNCTION__ Unop.pp op
@@ -391,8 +393,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
391393
| ShrL -> Bitv.lshr t1 t2
392394
| Rem -> Bitv.rem t1 t2
393395
| RemU -> Bitv.rem_u t1 t2
394-
| Rotl -> Bitv.rotate_left t1 t2
395-
| Rotr -> Bitv.rotate_right t1 t2
396+
| Ext_rotl -> Bitv.ext_rotate_left t1 t2
397+
| Ext_rotr -> Bitv.ext_rotate_right t1 t2
396398
| op ->
397399
Fmt.failwith {|%s: Unsupported %s operator "%a"|} __MODULE__
398400
__FUNCTION__ Binop.pp op

‎src/smtml/mappings.nop.ml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -271,6 +271,10 @@ module M = struct
271271

272272
let rotate_right _ = assert false
273273

274+
let ext_rotate_left _ = assert false
275+
276+
let ext_rotate_right _ = assert false
277+
274278
let nego _ = assert false
275279

276280
let addo ~signed:_ = assert false

‎src/smtml/mappings_intf.ml‎

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -471,11 +471,18 @@ module type M = sig
471471
[t1] and [t2]. *)
472472
val rem_u : term -> term -> term
473473

474-
(** [rotate_left t1 t2] constructs the left rotation of [t1] by [t2]. *)
475-
val rotate_left : term -> term -> term
474+
(** [rotate_left n t] constructs the left rotation of [t] by [n]. *)
475+
val rotate_left : int -> term -> term
476476

477-
(** [rotate_right t1 t2] constructs the right rotation of [t1] by [t2]. *)
478-
val rotate_right : term -> term -> term
477+
(** [rotate_right n t] constructs the right rotation of [t] by [n]. *)
478+
val rotate_right : int -> term -> term
479+
480+
(** [ext_rotate_left t1 t2] constructs the left rotation of [t1] by [t2]. *)
481+
val ext_rotate_left : term -> term -> term
482+
483+
(** [ext_rotate_right t1 t2] constructs the right rotation of [t1] by [t2].
484+
*)
485+
val ext_rotate_right : term -> term -> term
479486

480487
(** [nego t] constructs a predicate that checks that whether the bit-wise
481488
negation of [t] does not overflow. *)

‎src/smtml/ty.ml‎

Lines changed: 18 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -151,6 +151,8 @@ module Unop = struct
151151
| Regexp_plus
152152
| Regexp_opt
153153
| Regexp_comp
154+
| Rotl of int
155+
| Rotr of int
154156
[@@deriving ord]
155157

156158
let hash = function
@@ -188,6 +190,8 @@ module Unop = struct
188190
| Regexp_plus -> 25
189191
| Regexp_opt -> 26
190192
| Regexp_comp -> 27
193+
| Rotl n -> combine 28 n
194+
| Rotr n -> combine 29 n
191195

192196
let equal o1 o2 =
193197
match (o1, o2) with
@@ -220,11 +224,12 @@ module Unop = struct
220224
| Regexp_opt, Regexp_opt
221225
| Regexp_comp, Regexp_comp ->
222226
true
227+
| Rotl a, Rotl b | Rotr a, Rotr b -> a = b
223228
| ( ( Neg | Not | Clz | Popcnt | Ctz | Abs | Sqrt | Is_normal | Is_subnormal
224229
| Is_negative | Is_positive | Is_infinite | Is_nan | Is_zero | Ceil
225230
| Floor | Trunc | Nearest | Head | Tail | Reverse | Length | Trim
226231
| Regexp_star | Regexp_loop _ | Regexp_plus | Regexp_opt | Regexp_comp
227-
)
232+
| Rotl _ | Rotr _ )
228233
, _ ) ->
229234
false
230235

@@ -257,6 +262,8 @@ module Unop = struct
257262
| Regexp_plus -> Fmt.string fmt "+"
258263
| Regexp_opt -> Fmt.string fmt "opt"
259264
| Regexp_comp -> Fmt.string fmt "comp"
265+
| Rotl n -> Fmt.pf fmt "(rotl %d)" n
266+
| Rotr n -> Fmt.pf fmt "(rotr %d)" n
260267
end
261268

262269
module Binop = struct
@@ -279,8 +286,8 @@ module Binop = struct
279286
| Min
280287
| Max
281288
| Copysign
282-
| Rotl
283-
| Rotr
289+
| Ext_rotl
290+
| Ext_rotr
284291
| At
285292
| List_cons
286293
| List_append
@@ -315,8 +322,8 @@ module Binop = struct
315322
| Min -> 15
316323
| Max -> 16
317324
| Copysign -> 17
318-
| Rotl -> 18
319-
| Rotr -> 19
325+
| Ext_rotl -> 18
326+
| Ext_rotr -> 19
320327
| At -> 20
321328
| List_cons -> 21
322329
| List_append -> 22
@@ -351,8 +358,8 @@ module Binop = struct
351358
| Min, Min
352359
| Max, Max
353360
| Copysign, Copysign
354-
| Rotl, Rotl
355-
| Rotr, Rotr
361+
| Ext_rotl, Ext_rotl
362+
| Ext_rotr, Ext_rotr
356363
| At, At
357364
| List_cons, List_cons
358365
| List_append, List_append
@@ -366,8 +373,8 @@ module Binop = struct
366373
| Regexp_diff, Regexp_diff ->
367374
true
368375
| ( ( Add | Sub | Mul | Div | DivU | Rem | RemU | Shl | ShrA | ShrL | And
369-
| Or | Xor | Implies | Pow | Min | Max | Copysign | Rotl | Rotr | At
370-
| List_cons | List_append | String_prefix | String_suffix
376+
| Or | Xor | Implies | Pow | Min | Max | Copysign | Ext_rotr | Ext_rotl
377+
| At | List_cons | List_append | String_prefix | String_suffix
371378
| String_contains | String_last_index | String_in_re | Regexp_range
372379
| Regexp_inter | Regexp_diff )
373380
, _ ) ->
@@ -392,8 +399,8 @@ module Binop = struct
392399
| Min -> Fmt.string fmt "min"
393400
| Max -> Fmt.string fmt "max"
394401
| Copysign -> Fmt.string fmt "copysign"
395-
| Rotl -> Fmt.string fmt "rotl"
396-
| Rotr -> Fmt.string fmt "rotr"
402+
| Ext_rotl -> Fmt.string fmt "ext_rotl"
403+
| Ext_rotr -> Fmt.string fmt "ext_rotr"
397404
| At -> Fmt.string fmt "at"
398405
| List_cons -> Fmt.string fmt "cons"
399406
| List_append -> Fmt.string fmt "append"

0 commit comments

Comments
 (0)