Conversation
tautschnig
left a comment
There was a problem hiding this comment.
Is this being tested in any way? At least I don't trust my SMT-expression-building-code reading skills to be fully confident that the bswap code is completely correct.
| const std::size_t width = to_bitvector_type(expr.type()).get_width(); | ||
|
|
||
| // width must be multiple of bytes | ||
| if(width % 8 != 0) |
There was a problem hiding this comment.
Could config.ansi_c.char_width please be used so that #917 doesn't end up in an endless catch-up game?
There was a problem hiding this comment.
I did contemplate this; would the semantics of __builtin_bswapX actually change on a machine with chars that are >8 bits?
The gcc manual says "Byte here always means exactly 8 bits."
There was a problem hiding this comment.
I'd rather insist that exprt(ID_bswap) has a semantics that may differ from that of __builtin_bswapX; if there are cases where __builtin_bswapX does not swap bytes (of some number of bits) then it's up to the front-end to sort this out. If we want exprt(ID_bswap) to always swap multiples of 8 bits then we should 1) rename it and 2) change boolbvt::convert_bswap to follow this semantics.
The one case (TI C55x) of a non-8-bit-bytes architecture that I know of doesn't have GCC support so __builtin_bswapX wouldn't actually occur.
There was a problem hiding this comment.
Ok, then I'd advocate to make "number of bits in a byte" a parameter, so we don't rely on a global config.
There was a problem hiding this comment.
That could be done, but then we've still got byte_{extract,update} all the way to the back-end, which also need to know about the width of a byte. I'd just like to come up with a consistent solution for all of those.
There was a problem hiding this comment.
I'd probably go for the same here.
|
The existing tests for both features pass with Z3. Not tested with other solvers. |
Are those not actually in the repository, or how come no change to the tests was necessary/possible? (I would have expected some |
src/util/simplify_expr_int.cpp
Outdated
| // take apart | ||
| for(std::size_t bit=0; bit<width; bit+=8) | ||
| for(std::size_t bit = 0; bit < width; bit += bits_per_byte) | ||
| bytes.push_back((value >> bit)%256); |
There was a problem hiding this comment.
That needs to be amended as well: 256 should be power(2, bits_per_byte).
8de6a33 Merge pull request diffblue#2006 from tautschnig/opt-no-self-loops 6605699 Merge pull request diffblue#2217 from diffblue/c-preprocessing-cleanout f1d787b Merge pull request diffblue#2166 from tautschnig/out-of-bounds 25339d5 Add option not to transform self-loops into assumes 5e6a3af Merge pull request diffblue#2249 from tautschnig/attribute-used d3d888b Bounds check for flexible array members 41003e8 Handle negative byte_extract offsets efea5c4 Fix flattening of access beyond type-specified bounds 0ec87c8 Merge pull request diffblue#2271 from diffblue/letification 090790a Interpret GCC's attribute __used__ 7985716 Merge pull request diffblue#2252 from tautschnig/fresh-symbol-cleanup 022846a letify: use irep_hash_mapt when hashing is expensive 15dff7d Merge pull request diffblue#2260 from antlechner/antonia/annotation-class-value 9a0ffae added irep_hash_mapt da0adfe bugfix: irep_hash_containert now keeps a copy of the contained ireps 45436ce use std::size_t for container sizes 0c26a53 let_count_idt is now a struct e0a5142 Merge pull request diffblue#2206 from diffblue/use-get_identifier e0ad069 Add support for Java annotations with Class value 3817341 Merge pull request diffblue#2237 from smowton/smowton/feature/initialize-class-literals 25c097e use get_identifier() instead of get(ID_identifier) on symbols 4eda8ad Java class literals: init using a library hook when possible 70f13f3 Merge pull request diffblue#1906 from tautschnig/missing-return-semantics 57885a5 Merge pull request diffblue#1868 from tautschnig/fix-1867 b49822e Merge pull request diffblue#2028 from tautschnig/regression-fix 2815e84 Merge pull request diffblue#2259 from smowton/smowton/feature/note-abstract-methods 09b8cf7 Merge pull request diffblue#2014 from tautschnig/cadical-experiment f50237b Merge pull request diffblue#1967 from romainbrenguier/refactor/drop-constraint-inheritance2 3f951dd Merge pull request diffblue#2234 from nmanthey/upstream-fpr c6c2928 Drop inheritance from constraint on exprt 0ffd0ae Replace negation of constraint by a method f653dec use compiler defaults for gcc defines a31f530 remove need to do preprocessing on 16-bit test 24210e9 enable AWS Codebuild to do -m32 bfae4e3 enable Travis to do -m32 34a3d85 Merge pull request diffblue#2247 from antlechner/antonia/annotation-conversion 15ed961 Note when symbol-table entries are abstract methods 3a7135a Add module_dependencies.txt in test folder 1fa0b97 Generalize and rename does_annotation_exist 1db0af4 Define inverse function of convert_annotations ff25b2c get_max: do not parse every symbol name in the symbol table b603703 Add missing override 70da606 Merge pull request diffblue#2251 from tautschnig/rename-cleanup 49429cf Merge pull request diffblue#2257 from owen-jones-diffblue/owen-jones-diffblue/fix-cmake-macro 4b7a195 Improve naming of annotation variables 57d96e5 Fix CMake macro f9058e7 Merge pull request diffblue#2246 from diffblue/z3-fpa 6b0f265 Merge pull request diffblue#2248 from thk123/bugfix/doxygen-including-jbmc 72e99a0 Merge pull request diffblue#2201 from diffblue/remove-incomplete-type-constructors d4abbea smt2 implementation for popcount_exprt e8fa1c9 bswap_exprt now knows how many bits a byte has a6652d2 Merge pull request diffblue#2255 from tautschnig/speedup-no-pointer-check 4b0a2d6 goto_check: do not unnecessarily build size-of expressions 1fe7cd7 remove mathematical_typet() constructor, which produces an incomplete object 25d393b remove vector_typet() constructor, which produces an incomplete object e7c52e4 remove range_typet() constructor, which produces an incomplete object f92083d remove array_typet() constructor, which produces an incomplete object 72f63f3 remove tag_typet() constructor, which produces an incomplete object 516ed14 remove symbol_typet() constructor, which produces an incomplete object 4215f21 Consistently use get_fresh_aux_symbol instead of local implementations e6cd488 Remove unused goto_symext::new_name c24b820 Remove goto_convertt::lookup a816b26 Do not include rename.h when not using its functions 52ab088 called_functions: use unordered_set 157a12c Fix doxyfile to include JBMC documentation 026e93f function-pointer-removal: drop unused set b75fcbc smt2 implementation for bswap_exprt e276b27 Avoid extern/parameter name collisions in show-goto-functions/dump-c output 87c5948 C front-end: Record extern declarations in current scope a47941d perf-test: add -W/--witness-check to validate SV-COMP witness checking 5b0395f perf-test: Update Ubuntu AMI ids for latest version 1288ec7 perf-test: speed up builds just like e7bb127 did afccaec Provide goto-cc in performance tests f802d87 Support CaDiCaL in performance tests, remove redundant script 7872f7c Replace a missing return value by nondet 829068f Don't require the simplifier to solve this regression test git-subtree-dir: cbmc git-subtree-split: 8de6a33
This adds the encoding of bswap and popcount to the SMT2 back-end