6 ms·
Integer overflow and SMT-solvers
- petters 8y ago> Unsigned int should be used instead of int for "num", but many programmers use int as a generic type for everything. Yes, this is very common. For example, Google requires that C++ code always uses int instead of unsigned.
- raverbashing 8y agoYeah, this is stupid. If the language creators put a feature there, use it. I really don't buy the love that some have for using signed variables when they don't make sense. As a start, you only need one comparison to check if it's within range, as it's always > 0
- andrewflnr 8y agoNot using a feature because it's broken by default is perfectly valid. All those style guides that mandate signed ints do so because someone got burned by an overflow that wasn't caught.
- raverbashing 8y agoUnsigned are not broken by default, and I've been bitten much more by ints that overflow and go negative. Funny how that's not "broken by default" (it isn't) to the same people.
- smaddox 8y agoThese sorts of bugs seem like an inherent side effect of implicitness, in this case of implicit type casting in C/C++. Rust mostly solves this specific class of bugs by requiring explicit type casts. As a consequence, in Rust, unlike in C/C++, it is idiomatic to use an unsigned integer when negative values are semantically invalid. Rust also makes it fairly easy to define a `newtype` wrapper, for when you need semantics different from the primitive types. You can, for example, define an integer wrapper that always panics on overlow (as opposed to only in debug builds, which is the default for Rust). Recently, I've used this pattern to define a networking "sequence number" type that does not implement ordering operators (less than, greater than, etc.), but instead provides `older_than`, `newer_than`, etc. I made the switch after correcting multiple bugs caused by implicit and incorrect assumptions of total ordering; making the switch uncovered several more of such bugs . Of course, such a pattern is possible in C/C++ as well, but it is not as ergonomic and thus not as common.
- mcguire 8y ago"If you want to catch overflows on unsigned variables, use unsigned Z3 operations instead of signed, and do zero extend instead of sign extend."
- OpenBSD-reich2 8y agoSPARK exists, we don't need Rust. Most evangelized/shilled technology since systemd tbh.
- giornogiovanna 8y agoYou can (and in my opinion, should) take this further with range types, such as those implemented in Ada.
- smaddox 8y agoYeah, Rust doesn't have built-in range types, but it's fairly straightforward to write a macro to generate them. I've done this for array indices being passed over the network, in order to automate validation and minimize their bit-size on the wire.
- mcguire 8y agoInteresting; I'll have to takea closet look at https://yurichev.com/writings/SAT_SMT_by_example.pdf https://yurichev.com/writings/SAT_SMT_by_example.pdf. If you've heard of Frama-C, these issues are highlighted by automatically inserted checks.
- glangdale 8y agoStrongly recommend. The learning curve on SMT is steep (at least it seemed so to me; perhaps I'm not so bright?) but Dennis's work really helps with a lot of nice examples of non-trivial problems being solved with SMT.
- pjmlp 8y agoSomething like Frama-C should be compulsory in "Safe C", but alas.
- userbinator 8y agomalloc() will crash on too big input value, because malloc() takes unsigned size_t on input. Will it, or will it just fail and return null (which may crash later code if it doesn't check)? I believe the spec mandates the latter.
- loeg 8y agoAre you suggesting C mandates operating systems not overcommit memory (I don't think it does), or that objects cannot be larger than PTRDIFF_MAX (and ptrdiff_t is signed)? (Edit: On further reading, I don't think the standard says that, either.) Many implementations do not conform to that definition. But it's also possible that the expression results in a value smaller than PTRDIFF_MAX (or similarly, small enough the operating system does not need to overcommit), and then even a malloc conforming to that definition is free to return a pointer to some virtual memory (committed or not).
- zokier 8y agoWhile C integer rules are bit too arcane for me to remember, isn't the conversion from unsigned to signed integer in __addvsi3 undefined if the sum is greater than INT_MAX? If it is, the whole function is pretty much useless as compiler can optimize it to just plain addition.