Replace ocaml integer values with arbitrary-precision integers (#658)#660
Open
filipeom wants to merge 1 commit into
Open
Replace ocaml integer values with arbitrary-precision integers (#658)#660filipeom wants to merge 1 commit into
filipeom wants to merge 1 commit into
Conversation
📝 WalkthroughSummary by CodeRabbit
WalkthroughChangesZarith integer migration
Estimated code review effort: 4 (Complex) | ~45 minutes Suggested reviewers: 🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 7
🧹 Nitpick comments (2)
src/smtml/smtlib.ml (1)
105-106: 🩺 Stability & Availability | 🔵 Trivial | ⚡ Quick winDo not catch all exceptions as “invalid int.”
The
with _branch can mask unrelated failures raised byExpr.value, making programming errors appear to be malformed input. Reuse the existingz_of_string_opthelper so only integer parsing failure follows this error path.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@src/smtml/smtlib.ml` around lines 105 - 106, Update the integer parsing expression around Expr.value to use the existing z_of_string_opt helper, branching only when conversion fails and preserving the invalid-int error for malformed input. Remove the catch-all exception handler so unrelated Expr.value failures propagate normally.Source: Path instructions
src/smtml/eval.mli (1)
62-66: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winDocument all changed public interface declarations.
The changed
.mlientries below expose new or modifiedZ.tcontracts but lack odoc documentation. Add concise descriptions of their arbitrary-precision semantics and boundary behavior.
src/smtml/eval.mli#L62-L66: documentraw_binopandraw_relop.src/smtml/dolmenexpr_to_expr.mli#L57-L57: documentDolmenIntf.int.src/smtml/dolmenexpr_to_expr.mli#L110-L110: documentDolmenIntf.Interp.to_int.src/smtml/typed.mli#L148-L148: documentTyped.Int.v.As per path instructions, interface files should have complete odoc documentation for all public functions.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@src/smtml/eval.mli` around lines 62 - 66, Add concise odoc comments for raw_binop and raw_relop in src/smtml/eval.mli lines 62-66, documenting arbitrary-precision Z.t operation semantics and boundary behavior; document DolmenIntf.int at src/smtml/dolmenexpr_to_expr.mli line 57 and DolmenIntf.Interp.to_int at line 110, including their Z.t conversion semantics and boundaries; document Typed.Int.v in src/smtml/typed.mli line 148 with its arbitrary-precision and boundary behavior. Ensure all changed public declarations have complete interface documentation.Source: Path instructions
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@src/smtml/eval.ml`:
- Around line 173-175: Prevent oversized Z.t values from reaching Z.to_int
without validation across the affected sites: in src/smtml/eval.ml lines
173-175, 373-400, 422-425, and 476-492, route invalid shift, string/list index,
and String_from_code conversions through the evaluator’s existing error
handling; in src/smtml/expr.ml lines 395-400, replace assert false for invalid
constant-folded list indices with the appropriate error result; in
src/smtml/typed.ml lines 257-271, safely convert or modulo-reduce large rotation
counts before constructing Rotl or Rotr.
In `@src/smtml/parser.mly`:
- Around line 127-128: Update the Ty_bitv 32 and Ty_bitv 64 branches in the
parser’s decimal bitvector literal handling to use unsigned Z.t conversion, such
as Bitvector.make or the corresponding unsigned conversion functions. Preserve
the intended bit pattern for values above the signed range, including valid
values like 4294967295 for 32-bit vectors.
- Line 74: Update the parser actions in parser.mly for POP, pointer offsets,
rotation counts, and extract bounds to validate each Z.t operand is within the
target machine integer range before calling Z.to_int or Int32.of_int. Ensure
out-of-range values are converted into the parser’s normal failure path handled
by parse_with_error, rather than allowing Z.Overflow to escape.
In `@src/smtml/typed.ml`:
- Line 2264: Extend Mappings.Encoder.Int_impl.unop to handle the Abs operation
emitted by typed.ml’s abs function, producing the corresponding symbolic
absolute-value term instead of rejecting it. Preserve the existing Neg encoding
and unsupported-operation behavior for other unary integer operations.
In `@test/regression/test_issue_658.ml`:
- Around line 97-98: Update the Alcotest assertion description in the equality
test around Typed.Int.eq to describe that the equality evaluation is false,
rather than stating the numeric inequality being compared. Keep the expected
Typed.Bool.false_ result unchanged.
- Line 19: Replace the wildcard branch’s assert false in the equality regression
test with a runtime-safe false result, preserving the test’s intended behavior
when equality does not fold. Use the surrounding test expression to ensure the
branch reports failure without relying on an unreachable-case assertion.
- Around line 105-107: Update the callbacks passed to Alcotest.check_raises
around the negative-exponent pow cases to end with () after invoking
Typed.Int.(pow ...), removing assert false so check_raises can directly report a
missing Eval_error. Apply the same change to both referenced test cases.
---
Nitpick comments:
In `@src/smtml/eval.mli`:
- Around line 62-66: Add concise odoc comments for raw_binop and raw_relop in
src/smtml/eval.mli lines 62-66, documenting arbitrary-precision Z.t operation
semantics and boundary behavior; document DolmenIntf.int at
src/smtml/dolmenexpr_to_expr.mli line 57 and DolmenIntf.Interp.to_int at line
110, including their Z.t conversion semantics and boundaries; document
Typed.Int.v in src/smtml/typed.mli line 148 with its arbitrary-precision and
boundary behavior. Ensure all changed public declarations have complete
interface documentation.
In `@src/smtml/smtlib.ml`:
- Around line 105-106: Update the integer parsing expression around Expr.value
to use the existing z_of_string_opt helper, branching only when conversion fails
and preserving the invalid-int error for malformed input. Remove the catch-all
exception handler so unrelated Expr.value failures propagate normally.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro Plus
Run ID: edb2dbf6-00bb-4b95-8a26-5f5b03915e9b
📒 Files selected for processing (31)
docs/examples/dunedocs/examples/product_mix.mlsrc/smtml/bitwuzla_mappings.default.mlsrc/smtml/cvc5_mappings.default.mlsrc/smtml/dolmenexpr_to_expr.mlsrc/smtml/dolmenexpr_to_expr.mlisrc/smtml/eval.mlsrc/smtml/eval.mlisrc/smtml/expr.mlsrc/smtml/lexer.mllsrc/smtml/mappings.mlsrc/smtml/mappings_intf.mlsrc/smtml/parser.mlysrc/smtml/smtlib.mlsrc/smtml/typed.mlsrc/smtml/typed.mlisrc/smtml/value.mlsrc/smtml/value.mlisrc/smtml/z3_mappings.default.mltest/dunetest/integration/test_bindings.mltest/integration/test_optimizer.mltest/integration/test_solver.mltest/regression/dunetest/regression/test_issue_658.mltest/regression/test_regression.mltest/test_harness.mltest/unit/test_eval.mltest/unit/test_expr.mltest/unit/test_model.mltest/unit/test_smtlib_pp.ml
filipeom
force-pushed
the
filipe/issue-658
branch
from
July 25, 2026 11:26
b4458d4 to
38925f5
Compare
filipeom
force-pushed
the
filipe/issue-658
branch
from
July 25, 2026 13:54
38925f5 to
483d64a
Compare
There was a problem hiding this comment.
Actionable comments posted: 1
🧹 Nitpick comments (2)
test/regression/test_issue_ext_rotate.ml (1)
38-82: 🎯 Functional Correctness | 🔵 Trivial | ⚡ Quick winAdd a non-power-of-two normalization regression.
All current cases use 8- or 32-bit widths, so they cannot distinguish modulo normalization from the previous bitmask implementation. Add a direct case such as
normalize_shift_amount (Z.of_int (-3)) 10 = 7.As per path instructions, test files should cover edge cases and error paths, not only happy paths.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@test/regression/test_issue_ext_rotate.ml` around lines 38 - 82, Add a regression test for the non-power-of-two case by directly exercising normalize_shift_amount with Z.of_int (-3) and width 10, asserting the normalized result is 7. Place it alongside the existing rotation normalization tests and cover this edge case without changing the current power-of-two rotation cases.Source: Path instructions
src/smtml/typed.ml (1)
260-277: 🩺 Stability & Availability | 🔵 Trivial | ⚡ Quick winAvoid unchecked
assert falsebranches inBitv.Makesrc/smtml/typed.ml:260-277
Bitv.Makeis publicly exported, andWidth.tyis onlyTy.t, so a non-bitvector instantiation can hit these branches. Constrain the functor invariant or raiseFmt.failwithfor unsupported types instead.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@src/smtml/typed.ml` around lines 260 - 277, Update the type handling in Bitv.Make’s ext_rotate_left and ext_rotate_right implementations to avoid unchecked assert false branches when ty is not Ty_bitv. Enforce the functor’s bitvector invariant if supported by the API, or replace these branches with Fmt.failwith while preserving the existing normalization behavior for bitvector types.Source: Path instructions
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@src/smtml/bitvector.mli`:
- Around line 82-85: Complete the odoc comment for normalize_shift_amount by
adding `@param` documentation for n and width, an `@return` description for the
normalized int result, and the positive-width precondition if required by the
function contract. Keep the existing behavior description intact.
---
Nitpick comments:
In `@src/smtml/typed.ml`:
- Around line 260-277: Update the type handling in Bitv.Make’s ext_rotate_left
and ext_rotate_right implementations to avoid unchecked assert false branches
when ty is not Ty_bitv. Enforce the functor’s bitvector invariant if supported
by the API, or replace these branches with Fmt.failwith while preserving the
existing normalization behavior for bitvector types.
In `@test/regression/test_issue_ext_rotate.ml`:
- Around line 38-82: Add a regression test for the non-power-of-two case by
directly exercising normalize_shift_amount with Z.of_int (-3) and width 10,
asserting the normalized result is 7. Place it alongside the existing rotation
normalization tests and cover this edge case without changing the current
power-of-two rotation cases.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro Plus
Run ID: 620f2cf0-5d29-4056-9841-fffb68aa08b1
📒 Files selected for processing (36)
README.mddocs/examples.mlddocs/examples/dunedocs/examples/product_mix.mlsrc/smtml/bitvector.mlsrc/smtml/bitvector.mlisrc/smtml/bitwuzla_mappings.default.mlsrc/smtml/cvc5_mappings.default.mlsrc/smtml/dolmenexpr_to_expr.mlsrc/smtml/dolmenexpr_to_expr.mlisrc/smtml/eval.mlsrc/smtml/eval.mlisrc/smtml/expr.mlsrc/smtml/lexer.mllsrc/smtml/mappings.mlsrc/smtml/mappings_intf.mlsrc/smtml/parser.mlysrc/smtml/smtlib.mlsrc/smtml/typed.mlsrc/smtml/typed.mlisrc/smtml/value.mlsrc/smtml/value.mlisrc/smtml/z3_mappings.default.mltest/dunetest/integration/test_bindings.mltest/integration/test_optimizer.mltest/integration/test_solver.mltest/regression/dunetest/regression/test_issue_658.mltest/regression/test_issue_ext_rotate.mltest/regression/test_regression.mltest/test_harness.mltest/unit/test_eval.mltest/unit/test_expr.mltest/unit/test_model.mltest/unit/test_smtlib_pp.ml
🚧 Files skipped from review as they are similar to previous changes (32)
- docs/examples.mld
- README.md
- test/unit/test_model.ml
- src/smtml/typed.mli
- src/smtml/value.mli
- docs/examples/product_mix.ml
- test/unit/test_smtlib_pp.ml
- test/integration/test_bindings.ml
- src/smtml/bitwuzla_mappings.default.ml
- src/smtml/mappings_intf.ml
- src/smtml/eval.mli
- test/unit/test_eval.ml
- src/smtml/lexer.mll
- src/smtml/dolmenexpr_to_expr.mli
- docs/examples/dune
- src/smtml/dolmenexpr_to_expr.ml
- test/integration/test_optimizer.ml
- src/smtml/smtlib.ml
- src/smtml/z3_mappings.default.ml
- test/dune
- test/test_harness.ml
- test/regression/dune
- src/smtml/parser.mly
- src/smtml/mappings.ml
- test/unit/test_expr.ml
- src/smtml/cvc5_mappings.default.ml
- src/smtml/expr.ml
- test/regression/test_regression.ml
- src/smtml/value.ml
- test/integration/test_solver.ml
- test/regression/test_issue_658.ml
- src/smtml/eval.ml
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.
Closes #658