Write symbolic value at symbolic index #151

Stevengre · 2025-06-23T14:39:49Z

No description provided.

src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md

…ations.md

…WB operations. Update test data to include symbolic index value handling in storeBytes. Adjust formatting for clarity.

src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md

…ing a boolean wrapper for symbolic writes. This update includes detailed explanations of termination control, reordering for optimization, and write consolidation strategies. Adjusted comments for clarity and improved documentation.

src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md

tothtamas28 · 2025-06-25T08:47:23Z

src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md

+  rule #WB(true,  I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [simplification, concrete(I)]
+
+  // Reordering for Optimization
+  rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) [simplification]


Is a requires clause missing here?

We don't need requires clause there. It push uncompleted #WB down to the completed one with true as its first argument.

If so, why is it sound to reorder writes unconditionally, in particular, to the same index but with different values?

Because the Write Consolidation simplification rules have higher priority.

That unfortunately is not a mandatory directive for the backends: https://github.com/runtimeverification/k/blob/c829b1099ad225400bea5bcd5e9a21905060db06/docs/user_manual.md?plain=1#L1405-L1414

In that case, I feel there might be some issues. If we add requires here, there could be situations where we cannot determine whether I0 and I1 are equal. This could lead to #WB that can never be completed. Because simplification rules also don't generate branches.

In fact, I want this rule to work like owise to tackle uninterpreted cases. Even though this cannot be the default case, we still need an owise to cover all situations.

Suggested change

rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) [simplification]

rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) [simplification]

requires I0 =/=Int I1

As discussed on slack, the rule here is probably unsound when the written bytes overlap.
Example:
#WB(false, 0, 65535, 2, #WB( true, 1, 0, 1, bytes(b"\x00\x00")))
I can evaluate this directly to #WB(false, 0, 65535, 2, bytes(b"\x00\x00")) and then bytes(b"\xFF\xFF").
However, I could apply the simplification and get
#WB( true, 1, 0, 1, #WB(false, 0, 65535, 2, bytes(b"\x00\x00")))
but that would be #WB(true, 1, 0, 1, bytes(b"\xFF\xFF")) and then bytes(b"\xFF\x00")

Added the suggested constraints on this rule.

…termination control, reordering for optimization, and write consolidation strategies. Update code examples for better understanding and consistency.

… Update documentation to emphasize the reordering optimization and the specific rule for merging operations with identical indices. Improve code examples for better clarity.

…ed the placement of the `requires` clause for clarity and consistency in simplification rules.

Stevengre · 2025-07-07T03:09:55Z

Hi @tothtamas28!

I tried adding the I0 =/= Int I1 constraints to that simp rule, but it caused src/tests/integration/test-data/specs/store-symbolic-index-value.k to fail. This indicates that the test effectively captures the simp rule's behavior. If the backend's handling of this situation changes in the future, we'll be able to catch it during our version update CI.

…ration rule for better handling of overlapping writes. Update test data to ensure no overlapping writes between different indices, improving clarity and correctness in the specifications.

…s. Update documentation to clarify the edge case for identical indices, ensuring operations are marked complete to prevent infinite rewriting cycles. Adjust simplification annotation for improved clarity.

jberthold

Overall LGTM.
I left a few suggestions for improvements, but not necessarily on this same PR, could be done later if there are good reasons to merge this quickly.
I leave the approval to @tothtamas28 as I am unfamiliar with the surrounding code.

jberthold · 2025-07-08T10:24:09Z

src/tests/integration/test-data/specs/store-symbolic-index-value.k

+        (4 <=Int I0 orBool I0 +Int 4 <=Int 0) andBool
+        (4 <=Int I1 orBool I1 +Int 4 <=Int 0) andBool
+        (4 <=Int I2 orBool I2 +Int 4 <=Int 0) andBool


I think it is not very common to have so many orBool in the path condition.
Maybe you can make a few more tests, positive and negative (e.g. one like the counterexample I had) and replace the orBool conditions by more tests with one condition each?

Done!

f8f74fd

src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md

jberthold · 2025-07-08T10:37:17Z

src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md

+The rule below handles a termination edge case: it immediately marks the operation as complete with reduced priority to avoid infinite rewriting cycles.
+
+```k
+  rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B)) [simplification(60)]


This rule might fire if the one above is not applied for random reasons, for instance SMT solver timeout. However, it will just cut the simplification short so it is sound.

…to ensure truly non-overlapping writes. Update comments for improved clarity on index constraints and their relationships.

Co-authored-by: Jost Berthold <jost.berthold@gmail.com>

…-counter specification to clarify handling of perfect overlapping writes. Ensure that only the covering write is retained in the output, enhancing clarity on index relationships.

Write symbolic value at symbolic index

9c374d1

Stevengre requested a review from tothtamas28 June 23, 2025 14:39

Stevengre self-assigned this Jun 23, 2025

Set Version: 0.1.113

abb1cb8

Stevengre commented Jun 23, 2025

View reviewed changes

src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md Outdated Show resolved Hide resolved

Stevengre requested a review from jberthold June 23, 2025 14:46

jberthold reviewed Jun 24, 2025

View reviewed changes

src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md Outdated Show resolved Hide resolved

Stevengre added 5 commits June 24, 2025 09:36

Update src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplific…

3763e0b

…ations.md

fix

501ffb9

format

4903d42

Enhance simplification rules in RISC-V semantics for writeBytes and #…

273705b

…WB operations. Update test data to include symbolic index value handling in storeBytes. Adjust formatting for clarity.

delete uneccesary side condition

36f61a0

tothtamas28 reviewed Jun 24, 2025

View reviewed changes

src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md Show resolved Hide resolved

Stevengre added 2 commits June 25, 2025 10:44

bring ==Int to the require clause for more general cases

d95f68c

tothtamas28 reviewed Jun 25, 2025

View reviewed changes

Stevengre added 4 commits June 26, 2025 19:37

Refine documentation for #WB operations in RISC-V semantics. Clarify …

57f2421

…termination control, reordering for optimization, and write consolidation strategies. Update code examples for better understanding and consistency.

Clarify special case handling in #WB operations for RISC-V semantics.…

7d44f01

… Update documentation to emphasize the reordering optimization and the specific rule for merging operations with identical indices. Improve code examples for better clarity.

Add requires clause

a9988ce

Refactor #WB operation rule in RISC-V semantics documentation. Adjust…

b29dce7

…ed the placement of the `requires` clause for clarity and consistency in simplification rules.

Stevengre requested a review from tothtamas28 July 7, 2025 02:45

remove the require clause.

9b3d348

Enhance RISC-V semantics by adding a requires clause to the #WB ope…

9d8a051

…ration rule for better handling of overlapping writes. Update test data to ensure no overlapping writes between different indices, improving clarity and correctness in the specifications.

Stevengre requested a review from jberthold July 8, 2025 07:12

Refine termination handling in #WB operation rule for RISC-V semantic…

58d565a

…s. Update documentation to clarify the edge case for identical indices, ensuring operations are marked complete to prevent infinite rewriting cycles. Adjust simplification annotation for improved clarity.

jberthold reviewed Jul 8, 2025

View reviewed changes

Stevengre and others added 3 commits July 8, 2025 19:58

Refine requires clause in store-symbolic-index-value specification …

f8f74fd

…to ensure truly non-overlapping writes. Update comments for improved clarity on index constraints and their relationships.

One rule 4 perfect overlap

d8c0ad6

Co-authored-by: Jost Berthold <jost.berthold@gmail.com>

Update comments and requires clause in store-symbolic-index-overlap…

74eecca

…-counter specification to clarify handling of perfect overlapping writes. Ensure that only the covering write is retained in the output, enhancing clarity on index relationships.

tothtamas28 approved these changes Jul 8, 2025

View reviewed changes

Stevengre added the automerge label Jul 9, 2025

automergerpr-permission-manager bot merged commit 4df33d3 into master Jul 9, 2025
3 checks passed

automergerpr-permission-manager bot deleted the jh/sym-write-mem branch July 9, 2025 08:02

	rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) [simplification]
	rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) [simplification]
	requires I0 =/=Int I1

Write symbolic value at symbolic index #151

Write symbolic value at symbolic index #151

Conversation

Stevengre commented Jun 23, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Stevengre Jul 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Stevengre commented Jul 7, 2025

Uh oh!

jberthold left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Stevengre Jul 3, 2025 •

edited

Loading