TE
TechEcho
Home24h TopNewestBestAskShowJobs
GitHubTwitter
Home

TechEcho

A tech news platform built with Next.js, providing global tech news and discussions.

GitHubTwitter

Home

HomeNewestBestAskShowJobs

Resources

HackerNews APIOriginal HackerNewsNext.js

© 2025 TechEcho. All rights reserved.

Integer overflow and SMT-solvers

53 pointsby dennis714over 6 years ago

5 comments

smaddoxover 6 years ago
These sorts of bugs seem like an inherent side effect of implicitness, in this case of implicit type casting in C&#x2F;C++. Rust mostly solves this specific class of bugs by requiring explicit type casts. As a consequence, in Rust, unlike in C&#x2F;C++, it is idiomatic to use an unsigned integer when negative values are semantically invalid.<p>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&#x27;ve used this pattern to define a networking &quot;sequence number&quot; 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&#x2F;C++ as well, but it is not as ergonomic and thus not as common.
评论 #18527629 未加载
评论 #18529293 未加载
评论 #18528267 未加载
pettersover 6 years ago
&gt; Unsigned int should be used instead of int for &quot;num&quot;, but many programmers use int as a generic type for everything.<p>Yes, this is very common. For example, Google requires that C++ code always uses int instead of unsigned.
评论 #18529119 未加载
mcguireover 6 years ago
Interesting; I&#x27;ll have to takea closet look at <a href="https:&#x2F;&#x2F;yurichev.com&#x2F;writings&#x2F;SAT_SMT_by_example.pdf" rel="nofollow">https:&#x2F;&#x2F;yurichev.com&#x2F;writings&#x2F;SAT_SMT_by_example.pdf</a>.<p>If you&#x27;ve heard of Frama-C, these issues are highlighted by automatically inserted checks.
评论 #18529026 未加载
评论 #18529258 未加载
userbinatorover 6 years ago
<i>malloc() will crash on too big input value, because malloc() takes unsigned size_t on input.</i><p>Will it, or will it just fail and return null (which may crash later code if it doesn&#x27;t check)? I believe the spec mandates the latter.
评论 #18528925 未加载
zokierover 6 years ago
While C integer rules are bit too arcane for me to remember, isn&#x27;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.