Comments (6)
The problem is in calls like svUNeg i
which assumes the size represented with the given bit-size becomes non-negative in the code. Alas, this isn't true when i
is too small. -(-1) == -1 : :SInt 1
, -(-2) == -2 :: SInt 2
. Not a problem for 3
, since -(-3) == 3 :: SInt 3
Not hard to fix, but at the risk of generating ugly code for the most common case. I'm not even sure if it's worth supporting rotates with bit-vector second arguments.
Would it be a big deal for you if rotate
types changed so that the second argument is SInteger
? I think that would simplify a lot of the code. Same argument probably goes for shifts. Would love to hear what the end-user opinion is on this matter.
from sbv.
I feel that supporting bit-vector second arguments is useful, at least to me, as sometimes we may want to use SBV to verify hardware-related stuff where only bit-vectors but not mathematical numbers could be used.
We can definitely use sFromIntegral
to convert bit-vectors to SInteger
and then do the proposed new rotate
. However, I am unsure about the implementation in your mind, so I am worried if this would cause a mixture of theories, thus
- make many solvers that do not support LIA theories, e.g., boolector, cannot be used, and
- hugely hurts solving performance.
My current workaround is to convert both arguments to SWord
before doing the rotation and convert them back afterwards. This works under the assumption that the second argument is non-negative, and we add assertions for that. This is reasonable, as the Haskell standard library states that rotating with negative bits is undefined behavior.
For the fix, could we simply try to broaden the second argument to max(3, finiteBitSize)
bits internally as a preprocess procedure? It seems that this works, but I cannot confirm it without inspecting the actual implementation. This will only change the generated formula when the second argument is 1 or 2 bits, and will not have a huge impact on the performance.
ghci> prove $ \(a :: SInt 1) (b :: SInt 3) -> (sRotateRight a (xor b b)) .== a
Q.E.D.
ghci> prove $ \(a :: SInt 2) (b :: SInt 3) -> (sRotateRight a (xor b b)) .== a
Q.E.D.
ghci> prove $ \(a :: SInt 1) (b :: SInt 1) -> let b' = sFromIntegral b :: SInt 3 in (sRotateRight a (xor b' b')) .== a
Q.E.D.
from sbv.
@lsrcz OK; I pushed in a couple of tweaks; give it a test and see if it works for you.
This code is more complicated than I'd like; so if you can spare the cycles and figure out an easier way to code it up (especially if it still has bugs!) I'd appreciate PRs.
from sbv.
Thank you! I will test it and have a look at the code when I get some time.
from sbv.
Thank you, @LeventErkok, for the patch! The fix seems to work for me, as it survived some random testing.
I will leave the issue open to remind me to have a look at the code sometime.
from sbv.
I think this is good now; so I'm going to close it. If you find further issues, please open a new ticket
from sbv.
Related Issues (20)
- SBV->C: Support arbitrary size bit-vectors, and in general all(?) SBV types HOT 10
- Create `NonEmpty` instances for `EqSymbolic`, `OrdSymbolic`, `Mergeable`, etc.
- Set support for cvc5 HOT 1
- ExtractIO HOT 1
- Zombie process fixes HOT 5
- Tower example
- Q: Results of 'wpProveWith' HOT 2
- Generating `Num (SBV a)` instances "generically" HOT 10
- CFP case missing in the Eq instance for CVal HOT 5
- Unsound term simplification for ite with SFloatingPoint HOT 2
- FAQ: best practices for records? HOT 4
- Explore `Iso` instances
- Consider removing `Num a => Num (SBV a)` instance
- Make OptimizeResult type dependent on OptimizeStyle HOT 3
- Ranges over SIntegers HOT 4
- Let 'optimize' return variable values HOT 2
- Using uninterpreted functions in a quantified formula will not declare it in the top-level HOT 10
- Soft Question: Best approach for fixed size symbolic arrays HOT 13
- `checkSatWith` in analogy to `satWith` HOT 1
- Principle of least astonishment violated for symbolic types whose metric space type differs in representation HOT 9
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from sbv.