Soundness: short-circuit RHS assignments are treated as executed
维护者通常 2 天内回复
评估
调研方向
Start at RefinementTypeChecker.visitCtBinaryOperator and reproduce the false && and true || cases from the issue. Compare current main with the conservative fix in PR #257, then verify both operators, nested writes, and branches where the RHS runs or is skipped. Done means the invalid refinement is rejected without rejecting valid executed-RHS cases.
由索引模型根据 Issue 内容生成。
描述
Problem
A write in the right operand of Java && or || is applied to LiquidJava's variable context even when Java short-circuits and does not execute that operand. The verifier can then prove a refinement about a value the program never assigned.
Minimal reproducer
import liquidjava.specification.Refinement;
public class Repro {
public static void main(String[] args) {
int x = 0;
boolean ignored = false && ((x = 1) == 1);
@Refinement("_ == 1") int y = x; // should be a Refinement Error
assert y == 1; // fails: y is 0
}
}
Expected: Reject the refinement on y. Java skips the RHS of &&, so x remains 0.
Actual: Correct! Passed Verification. on main at dd02e996. Compiling and running the program with assertions enabled throws AssertionError. The analogous true || RHS path has the same conditional-execution rule.
Cause and scope
RefinementTypeChecker.visitCtBinaryOperator scans both operands before applying the binary operation refinement. A RHS assignment updates the context during that scan; the later operator check does not distinguish a definitely executed write from a conditionally executed one.
The closed PR #257 contains a reproducer and a conservative fix. The fix should be ported and reviewed against current main, including both operators, nested writes, and branches where the RHS runs or is skipped. Example tests now use // Expect: Refinement Error after #293.
- 主要语言
- Java
- 星标
- 67
- 派生
- 36
- 平均合并
- 3 天 16 小时
- 30 天内合并 PR
- 9
环境准备
- 没有 Dockerfile 或 Docker Compose 文件
- 有 Pull Request 模板
- 阅读贡献指南
从这里开始
- 先读完整个 Issue，再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 Issue 编号。
liquid-java/liquidjava 的其他 Issue
-
bug
难度 2/5 1-3 小时 新手友好度 78/100
liquid-java/liquidjava#321 ·
维护者通常 2 天内回复
-
bug
难度 3/5 1-2 天 新手友好度 76/100
liquid-java/liquidjava#322 ·
维护者通常 2 天内回复
-
Fields with the same name in different classes collide可能已有人在做 关联的 PR 仍在进行中或已合并。 未关闭bug
难度 4/5 3-5 天 新手友好度 52/100
liquid-java/liquidjava#318 ·
维护者通常 2 天内回复
-
Nested classes wipe the outer class's field refinements可能已有人在做 关联的 PR 仍在进行中或已合并。 未关闭bug
难度 4/5 3-5 天 新手友好度 55/100
liquid-java/liquidjava#317 ·
维护者通常 2 天内回复
-
Reading a field of a class declared later in the file loses its refinement可能已有人在做 关联的 PR 仍在进行中或已合并。 未关闭bug
难度 4/5 3-5 天 新手友好度 62/100
liquid-java/liquidjava#316 ·
维护者通常 2 天内回复
查看 liquid-java/liquidjava 的全部 Issue
相似的 Issue
-
Clarify Javadoc for Logger methods taking Object... arguments with regards to Throwable detection未关闭
难度 2/5 1-3 小时 新手友好度 68/100
-
难度 1/5 1-3 小时 新手友好度 88/100
-
[Bug] The shared instance selector's placeholder and no-match text ignore the display language可能已有人在做 关联的 PR 仍在进行中或已合并。 未关闭
难度 2/5 1-3 小时 新手友好度 90/100
apache/rocketmq-dashboard#5561 ·
维护者通常 3 天内回复
-
enhancement
难度 2/5 1-3 小时 新手友好度 68/100
维护者通常 1 天内回复
-
test(setup): GitHub configuration tests fail when the temp path is long enough for YAML folding可能已有人在做 关联的 PR 仍在进行中或已合并。 未关闭bug good first issue help wanted priority medium size S
难度 2/5 1-3 小时 新手友好度 84/100
martin-francois/symphony-trello#776 · 1 条评论 ·
维护者通常 1 天内回复