From e2c8131938328bb0c57ddd524fa653c1f510551d Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 10 Oct 2026 10:55:18 -0700 Subject: [PATCH 1/4] Document Kvasir option --dyncomp-unhandled-ops --- doc/CHANGELOG.md | 8 ++++++++ doc/daikon.texinfo | 14 ++++++++++++++ 2 files changed, 22 insertions(+) diff --git a/doc/CHANGELOG.md b/doc/CHANGELOG.md index 6db6daed42..c2c5dc5a4d 100644 --- a/doc/CHANGELOG.md +++ b/doc/CHANGELOG.md @@ -21,6 +21,14 @@ Further documentation can be found in: `make -C $DAIKONDIR/java javadoc` It is also available at . +## Version 5.9.1 (???, 2026) + +Fjalar/Kvasir: + +* New command-line option `--dyncomp-unhandled-ops=warn` makes DynComp + print a warning and continue, rather than stop, when it encounters a VEX IR + operation that it does not handle. + ## Version 5.9.0 (September 1, 2026) * All Daikon tools now work with Java 8-26. diff --git a/doc/daikon.texinfo b/doc/daikon.texinfo index 2c7d2f72e6..0ed0639b23 100644 --- a/doc/daikon.texinfo +++ b/doc/daikon.texinfo @@ -4691,6 +4691,20 @@ y} or @code{x != y}). (@option{=comparisons}) Finally, you may specify that no binary operations qualify as interactions between values. Thus, DynComp only tracks dataflow. (@option{=none}) +@item --dyncomp-unhandled-ops=panic +@item --dyncomp-unhandled-ops=warn + +By default, if DynComp encounters a Valgrind VEX IR operation that it +does not handle, it prints the name of the operation and stops. +(@option{=panic}) Please report such a failure (@pxref{Reporting problems}). + +Alternatively, DynComp can print a warning the first time it encounters +each such operation and continue, approximating the operation: the result +of an operation with one operand is comparable to its operand, and the +operands of an operation with more than one operand are made comparable to +one another. The resulting comparability sets may be larger than +necessary, but are not smaller. (@option{=warn}) + @item --dyncomp-approximate-literals This option applies an approximation for handling literal values which From a7f7f564968139d223f964245933b4073861a0dc Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 10 Oct 2026 12:19:44 -0700 Subject: [PATCH 2/4] Document and test Kvasir's --dyncomp-unhandled-ops option --- doc/daikon.texinfo | 18 ++++++++++++++++++ tests/kvasir-tests/FloatTest/Makefile | 3 +++ 2 files changed, 21 insertions(+) diff --git a/doc/daikon.texinfo b/doc/daikon.texinfo index 2c7d2f72e6..d3f1a965a9 100644 --- a/doc/daikon.texinfo +++ b/doc/daikon.texinfo @@ -4691,6 +4691,24 @@ y} or @code{x != y}). (@option{=comparisons}) Finally, you may specify that no binary operations qualify as interactions between values. Thus, DynComp only tracks dataflow. (@option{=none}) +@item --dyncomp-unhandled-ops=panic +@item --dyncomp-unhandled-ops=warn + +Kvasir translates the target program into Valgrind's VEX intermediate +representation. By default, DynComp stops with an error if the program +uses a binary, ternary, or quaternary VEX operator that DynComp does not +handle. (@option{=panic}) + +You may instead have DynComp print a warning, once per unhandled operator, +and approximate the operator. (@option{=warn}) The approximation +ignores operands that appear to be rounding modes, shift amounts, or lane +indices. It treats an operator that produces a boolean as a comparison +of its other operands. It treats any other operator as an interaction +among its other operands, unless @option{--dyncomp-interactions} is +@option{units} or @option{comparisons}, in which case it treats the +operator as a non-interaction. The resulting comparability sets may be +imprecise. + @item --dyncomp-approximate-literals This option applies an approximation for handling literal values which diff --git a/tests/kvasir-tests/FloatTest/Makefile b/tests/kvasir-tests/FloatTest/Makefile index 3783acf761..cc55e06e55 100644 --- a/tests/kvasir-tests/FloatTest/Makefile +++ b/tests/kvasir-tests/FloatTest/Makefile @@ -1,4 +1,7 @@ NAME := FloatTest CFLAGS := -Wno-overflow +# FloatTest uses only operators that DynComp handles, so this option must +# not change the results. +KVASIR_OPTIONS := --dyncomp-unhandled-ops=warn include ../Makefile.common From f26ed7fa489424d7da4187055bd9f2d7296cff67 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 10 Oct 2026 18:26:58 -0700 Subject: [PATCH 3/4] Make the --dyncomp-unhandled-ops documentation match Kvasir; drop the FloatTest use of the option The manual now describes when ternary and quaternary operators skip the check, the exact rule for treating a boolean-producing operator as a comparison, and the behavior under --dyncomp-interactions=none. It uses @itemx for the extra lines of a multi-line @item. FloatTest no longer passes =warn, which hid unhandled operators and required an unmerged Kvasir change. --- doc/daikon.texinfo | 40 +++++++++++++++++++-------- tests/kvasir-tests/FloatTest/Makefile | 3 -- 2 files changed, 29 insertions(+), 14 deletions(-) diff --git a/doc/daikon.texinfo b/doc/daikon.texinfo index 65c0814228..a59d7932c4 100644 --- a/doc/daikon.texinfo +++ b/doc/daikon.texinfo @@ -4672,9 +4672,9 @@ subsequent runs to reduce the time required to generate the @file{.trace} file(s). @item --dyncomp-interactions=all -@item --dyncomp-interactions=units -@item --dyncomp-interactions=comparisons -@item --dyncomp-interactions=none +@itemx --dyncomp-interactions=units +@itemx --dyncomp-interactions=comparisons +@itemx --dyncomp-interactions=none By default, DynComp considers any binary operation as an interaction between its two operands. (@option{=all}) @@ -4692,22 +4692,40 @@ Finally, you may specify that no binary operations qualify as interactions between values. Thus, DynComp only tracks dataflow. (@option{=none}) @item --dyncomp-unhandled-ops=panic -@item --dyncomp-unhandled-ops=warn +@itemx --dyncomp-unhandled-ops=warn By default, if DynComp encounters a binary, ternary, or quaternary Valgrind VEX IR operator that it does not handle, it prints the name of the operator and stops. (@option{=panic}) Please report such a failure -(@pxref{Reporting problems}). +(@pxref{Reporting problems}). When @option{--dyncomp-interactions} is +@option{comparisons} or @option{none}, DynComp treats every ternary and +quaternary operator as a non-interaction without examining it, so it +does not stop at (or warn about) an unhandled ternary or quaternary +operator. Alternatively, DynComp can print a warning the first time it encounters each such operator and continue, approximating the operator. (@option{=warn}) The approximation ignores operands that appear to be -rounding modes, shift amounts, or lane indices. It treats an operator -that produces a boolean as a comparison of its other operands. It -treats any other operator as an interaction among its other operands, -unless @option{--dyncomp-interactions} is @option{units} or -@option{comparisons}, in which case it treats the operator as a -non-interaction. The resulting comparability sets may be imprecise. +rounding modes, shift amounts, or lane indices; the remaining operands +are the data operands. The approximation is: + +@itemize @bullet +@item +If @option{--dyncomp-interactions} is @option{none}, the operator is a +non-interaction. +@item +Otherwise, if the operator produces a boolean and has exactly 2 data +operands, it is a comparison of those operands: they become comparable, +and the result is comparable to nothing. +@item +Otherwise, if @option{--dyncomp-interactions} is @option{units} or +@option{comparisons}, the operator is a non-interaction. +@item +Otherwise, the operator is an interaction: its data operands and its +result all become comparable. +@end itemize + +The resulting comparability sets may be imprecise. @item --dyncomp-approximate-literals diff --git a/tests/kvasir-tests/FloatTest/Makefile b/tests/kvasir-tests/FloatTest/Makefile index cc55e06e55..3783acf761 100644 --- a/tests/kvasir-tests/FloatTest/Makefile +++ b/tests/kvasir-tests/FloatTest/Makefile @@ -1,7 +1,4 @@ NAME := FloatTest CFLAGS := -Wno-overflow -# FloatTest uses only operators that DynComp handles, so this option must -# not change the results. -KVASIR_OPTIONS := --dyncomp-unhandled-ops=warn include ../Makefile.common From 4936791d2699a2007de133f78f599bd777e662bc Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 19 Oct 2026 11:53:21 -0700 Subject: [PATCH 4/4] Manual: --dyncomp-unhandled-ops also covers unary operators (codespecs/fjalar#87) --- doc/daikon.texinfo | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/doc/daikon.texinfo b/doc/daikon.texinfo index d2ca4835d8..999bb660c6 100644 --- a/doc/daikon.texinfo +++ b/doc/daikon.texinfo @@ -4501,7 +4501,7 @@ interactions between values. Thus, DynComp only tracks dataflow. (@option{=none @item --dyncomp-unhandled-ops=panic @itemx --dyncomp-unhandled-ops=warn -By default, if DynComp encounters a binary, ternary, or quaternary +By default, if DynComp encounters a unary, binary, ternary, or quaternary Valgrind VEX IR operator that it does not handle, it prints the name of the operator and stops. (@option{=panic}) Please report such a failure (@pxref{Reporting problems}). When @option{--dyncomp-interactions} is @@ -4512,9 +4512,11 @@ operator. Alternatively, DynComp can print a warning the first time it encounters each such operator and continue, approximating the operator. -(@option{=warn}) The approximation ignores operands that appear to be -rounding modes, shift amounts, or lane indices; the remaining operands -are the data operands. The approximation is: +(@option{=warn}) The result of a unary operator gets the tag of its +operand, as for a copy. For any other operator, the approximation +ignores operands that appear to be rounding modes, shift amounts, or +lane indices; the remaining operands are the data operands. The +approximation is: @itemize @bullet @item