fix transfer semantics for set/clear high/low bits

[dominicmkennedy]

there are incorrect op semantics for (in how the ops are lowered to the SMT dialect) SetHighBitsOp, SetLowBitsOp, ClearHighBitsOp, and ClearLowBitsOp, this PR fixes all of those

[dominicmkennedy]

I remove the functions set_high_bits and set_low_bits in xdsl_smt/utils/transfer_to_smt_util.py (bc they are wrong). But this seems to have broken xdsl_smt/passes/lower_to_smt/transfer_to_smt.py, but as far as I can tell this is just a very out of date version of xdsl_smt/semantics/transfer_semantics.py, should the old file just be removed? or am I missing something here?

[math-fehr]

Sorry, I was very busy during PLDI, and now I have more time.
Let me look at it on monday, I'll check what's going on!

And thanks a lot;)

[dominicmkennedy]

No worries, those paper deadlines are stressful!

[Hatsunespica]

Let's take the function set_high_bits as an example.
The original implementation assumes the input, high_bits, is always less than the bit width, which is the constraint at LLVM APInt this line: https://llvm.org/doxygen/APInt_8h_source.html#l01369
While this implementation assigns the semantic that when the incoming bitwidth is larger than the bit width, we should set all bits instead of a random value.

These are generated z3 exprs:
Function test is the old implementation while test1 is the one given in this PR

; You can edit this code!
; Click here and start typing.
(declare-datatypes ((Pair 2)) ((par (X Y) ((pair (first X) (second Y))))))

(declare-const x (_ BitVec 8))
(declare-const y (_ BitVec 8))
(declare-const c Bool)


(define-fun $test1 (($x (_ BitVec 8)) ($y (_ BitVec 8)) ($tmp Bool)) (Pair (_ BitVec 8) Bool)
  (let (($tmp_0 (_ bv8 8))) 
  (let (($tmp_1 (ite (bvult $y $tmp_0) $y $tmp_0))) 
  (let (($tmp_2 (_ bv1 8))) 
  (pair (bvor $x (bvshl (bvsub (bvshl $tmp_2 $tmp_1) $tmp_2) (bvsub $tmp_0 $tmp_1))) $tmp)))))

(define-fun $test (($x (_ BitVec 8)) ($y (_ BitVec 8)) ($tmp Bool)) (Pair (_ BitVec 8) Bool)
  (let (($tmp_0 (_ bv0 8))) 
  (let (($tmp_1 (bvsub (_ bv8 8) $y))) 
  (pair (bvor (bvlshr (bvshl (bvshl (bvashr (_ bv255 8) $tmp_1) $tmp_1) $tmp_0) $tmp_0) $x) $tmp))))

(assert (bvult y #x08))
(assert (distinct ($test1 x y c) ($test x y c)))
(check-sat)
(get-model)

(eval ($test x y c))
(eval ($test1 x y c))

It tries to find a counterexample when y<= 8 which is the bitwidth and it's unsat. If we release the constraint and it did find one.
So the problem is what's the semantic for get_high_width when the input provides more bits than the bit width

[Hatsunespica]

@math-fehr By the way, I found another small issue. https://github.com/opencompl/xdsl-smt/blob/main/xdsl_smt/passes/lower_to_smt/smt_lowerer_loaders.py#L72
At L72 it specifies rewriting patterns on transfer, while L67 provides transfer semantics. Maybe we could remove the one at L72? Because I think we have move all transfer semantics from the old rewriting patterns into semantics forms

[dominicmkennedy]

ah, good point! I guess from my point of view, all other operations in the transfer dialect are total functions (output is well-defined for all inputs) like how we have special gaurds for sdiv, udiv, etc. to make sure they're in line with the smt-lib version. So I was thinking that it should also be the case that setting/clearing high/low bits is also a total function

[math-fehr]

Yes @Hatsunespica, please remove the one you think we should remove!

[dominicmkennedy]

thanks for taking a look @math-fehr, can you also weigh in on the question about semantics? Is it okay if the transfer dialect has some ub semantics?

[math-fehr]

My understanding is that transfer should have ub and poison semantics, as it is supposedly modelling APInt. I am currently writing a similar version of transfer but that is exactly smt.bv with arbitrary bitwidth (so no UB or poison).

[dominicmkennedy]

😨😨 if that's the case then there are several semantically incorrect lowerings from the transfer dialect into lib-smt code (and some bad rewrite rules for the optimization passes). At least for ops like u/sdiv, u/srem, a/lshr, and shl (and maybe some other ops), since with LLVM's APInt's these ops have some undefined inputs (div by 0 etc.) but we lower to the lib-smt functions which are defined for all inputs, so they end up being more restrictive