Repository navigation
Conversation
expr2tags_Unop_DC now takes the operation and switches on it, like the binary, ternary, and quaternary functions do. Unary operations whose result is a boolean, or a mask or count computed from the operand's bits (CmpNEZ*, CmpwNEZ*, 32to1, 64to1, Clz*, Ctz*, PopCount*, GetMSBs*), give the result tag 0, as binary comparisons do. All other unary operations return the tag of the operand, as before. An operation that DynComp does not handle now reaches the default case for every arity. The new option --dyncomp-unhandled-ops=panic|warn controls what happens then. "panic" (the default) stops, as before. "warn" prints a warning once per operation and approximates the operation: a unary operation returns its operand's tag, and other operations merge their operands' tags.
|
Warning Review limit reached
This review includes 5 billable files and costs up to $1.25. Or wait 35 minutes for your next included review. View limit details
Comment |
… gets tag 0 Returning a constant tag discarded the operand's tag expression, so VEX removed it as dead code, along with any merge it performed. For example, in 'char lt = (a < b)' the merge of a and b was lost.
This was referenced Oct 10, 2026
Member
Author
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
expr2tags_Unop_DCused to ignore the operation: it returned the operand's tag for every unary operation, and its list of operations was only a comment. The binary, ternary, and quaternary functions instead switch on the operation and panic on one they do not handle. This pull request makes the arities consistent.Unary operations are now handled explicitly.
expr2tags_Unop_DCtakes the operation and switches on it. All 283 unary operations inVEX/priv/ir_defs.c(typeOfPrimop) are covered:Not,Neg, conversions, ...).The comment list contained two binary operations (
Iop_MulHi8Sx16,Iop_MulHi8Ux16); they are not unary cases.Boolean, mask, and count results get tag 0. Binary comparisons merge their operands' tags and give the result tag 0, because the result is a boolean. The unary operations
CmpNEZ*,CmpwNEZ*,32to1,64to1(booleans or lane masks) andClz*,Ctz*,PopCount*,GetMSBs*(counts or masks of the operand's bits) now do the same, instead of passing the operand's tag through. They do not simply return a constant tag 0, because then VEX would remove the operand's tag computation as dead code, together with any merge in it (such as the merge ofaandbinchar lt = (a < b)). Instead they pass the operand's tag to a new helper,MC_(helperc_RETURN_0), which returns 0.New option
--dyncomp-unhandled-ops=panic|warn. For every arity, an operation that DynComp does not handle reaches thedefaultcase, which callsreport_unhandled_op_DC:panic(the default) prints the operation and stops, as before.warnprints a warning once per operation and approximates it: a unary operation returns its operand's tag; a binary operation merges its operands' tags (except in--dyncomp-interactions=comparisonsmode); a ternary or quaternary operation merges all its operands' tags. Merging over-approximates comparability, which can hide no invariants.The option is listed in
--help, and./check-options-documentedpasses. codespecs/daikon#891 documents it in the Daikon manual.Testing:
./test-kvasir.sh(the DynComp and Kvasir regression tests) passes with no goal-file changes;make build(no new warnings); a small program usingstrlen,__builtin_ctz/clz/popcount, and comparisons produces.declsoutput identical to master's;--dyncomp-unhandled-ops=bogusis rejected.