mirror of
https://github.com/elicpeter/nyx.git
synced 2026-07-24 21:41:02 +02:00
a438886217
* refactor: Update comments for clarity and add expectations.json files for performance metrics * feat: Implement FP guard for JS/TS local-collection receivers to suppress missing ownership checks * feat: Enhance Rust parameter handling to classify local collections and prevent false ownership checks * refactor: Simplify code formatting for better readability in multiple files * refactor: Improve UTF-8 sequence length handling and enhance clarity in loop iteration * feat: Update Java and Python patterns to include new security rules * refactor: Improve comment clarity and consistency across multiple Rust files * refactor: Simplify code formatting for improved readability in integration tests and module files * refactor: Improve comment formatting and enhance clarity in assertions across multiple files
1086 lines
32 KiB
Rust
1086 lines
32 KiB
Rust
//! Comprehensive tests for the constraint solving module.
|
|
|
|
use super::domain::*;
|
|
use super::lower::*;
|
|
use super::solver::*;
|
|
use crate::ssa::const_prop::ConstLattice;
|
|
use crate::ssa::ir::SsaValue;
|
|
use std::collections::HashMap;
|
|
|
|
// ── ValueFact meet tests ────────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn valuefact_meet_eq_eq_same() {
|
|
let mut a = ValueFact::top();
|
|
a.exact = Some(ConstValue::Int(5));
|
|
let mut b = ValueFact::top();
|
|
b.exact = Some(ConstValue::Int(5));
|
|
let m = a.meet(&b);
|
|
assert_eq!(m.exact, Some(ConstValue::Int(5)));
|
|
assert!(!m.is_bottom());
|
|
}
|
|
|
|
#[test]
|
|
fn valuefact_meet_eq_eq_diff() {
|
|
let mut a = ValueFact::top();
|
|
a.exact = Some(ConstValue::Int(5));
|
|
let mut b = ValueFact::top();
|
|
b.exact = Some(ConstValue::Int(7));
|
|
let m = a.meet(&b);
|
|
assert!(m.is_bottom());
|
|
}
|
|
|
|
#[test]
|
|
fn valuefact_meet_eq_neq() {
|
|
let mut a = ValueFact::top();
|
|
a.exact = Some(ConstValue::Int(5));
|
|
let mut b = ValueFact::top();
|
|
b.excluded.push(ConstValue::Int(5));
|
|
let m = a.meet(&b);
|
|
assert!(m.is_bottom());
|
|
}
|
|
|
|
#[test]
|
|
fn valuefact_meet_gt_lt_contradiction() {
|
|
// x > 10 meet x < 5 → empty interval → bottom
|
|
let mut a = ValueFact::top();
|
|
a.lo = Some(10);
|
|
a.lo_strict = true;
|
|
let mut b = ValueFact::top();
|
|
b.hi = Some(5);
|
|
b.hi_strict = true;
|
|
let m = a.meet(&b);
|
|
assert!(m.is_bottom(), "expected bottom for (10,+inf) ∩ (-inf,5)");
|
|
}
|
|
|
|
#[test]
|
|
fn valuefact_meet_gt_lt_compatible() {
|
|
// x > 0 meet x < 100 → (0, 100) open interval
|
|
let mut a = ValueFact::top();
|
|
a.lo = Some(0);
|
|
a.lo_strict = true;
|
|
let mut b = ValueFact::top();
|
|
b.hi = Some(100);
|
|
b.hi_strict = true;
|
|
let m = a.meet(&b);
|
|
assert!(!m.is_bottom());
|
|
assert_eq!(m.lo, Some(0));
|
|
assert!(m.lo_strict);
|
|
assert_eq!(m.hi, Some(100));
|
|
assert!(m.hi_strict);
|
|
}
|
|
|
|
#[test]
|
|
fn valuefact_meet_null_nonnull_is_bottom() {
|
|
let mut a = ValueFact::top();
|
|
a.null = Nullability::Null;
|
|
let mut b = ValueFact::top();
|
|
b.null = Nullability::NonNull;
|
|
let m = a.meet(&b);
|
|
assert!(m.is_bottom());
|
|
}
|
|
|
|
// ── ValueFact join tests ────────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn valuefact_join_intervals_preserves_weaker() {
|
|
// [x > 0] join [x > 5] = [x > 0]
|
|
let mut a = ValueFact::top();
|
|
a.lo = Some(0);
|
|
a.lo_strict = true;
|
|
let mut b = ValueFact::top();
|
|
b.lo = Some(5);
|
|
b.lo_strict = true;
|
|
let j = a.join(&b);
|
|
assert_eq!(j.lo, Some(0));
|
|
assert!(j.lo_strict);
|
|
assert_eq!(j.hi, None); // no upper bound
|
|
}
|
|
|
|
#[test]
|
|
fn valuefact_join_exact_to_interval() {
|
|
// Eq(5) join Eq(7) = no exact, interval [5,7]
|
|
let mut a = ValueFact::top();
|
|
a.exact = Some(ConstValue::Int(5));
|
|
a.lo = Some(5);
|
|
a.hi = Some(5);
|
|
let mut b = ValueFact::top();
|
|
b.exact = Some(ConstValue::Int(7));
|
|
b.lo = Some(7);
|
|
b.hi = Some(7);
|
|
let j = a.join(&b);
|
|
assert_eq!(j.exact, None); // different constants
|
|
assert_eq!(j.lo, Some(5));
|
|
assert_eq!(j.hi, Some(7));
|
|
}
|
|
|
|
#[test]
|
|
fn valuefact_join_nonnull_and_unknown() {
|
|
let mut a = ValueFact::top();
|
|
a.null = Nullability::NonNull;
|
|
let b = ValueFact::top(); // null = Unknown
|
|
let j = a.join(&b);
|
|
assert_eq!(j.null, Nullability::Unknown);
|
|
}
|
|
|
|
#[test]
|
|
fn valuefact_join_nonnull_and_nonnull() {
|
|
let mut a = ValueFact::top();
|
|
a.null = Nullability::NonNull;
|
|
let mut b = ValueFact::top();
|
|
b.null = Nullability::NonNull;
|
|
let j = a.join(&b);
|
|
assert_eq!(j.null, Nullability::NonNull);
|
|
}
|
|
|
|
// ── ValueFact widen tests ───────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn valuefact_widen_unstable_bound() {
|
|
let mut a = ValueFact::top();
|
|
a.lo = Some(0);
|
|
a.lo_strict = true;
|
|
let mut b = ValueFact::top();
|
|
b.lo = Some(5); // changed from 0 to 5
|
|
b.lo_strict = true;
|
|
let w = a.widen(&b);
|
|
assert_eq!(w.lo, None); // dropped because unstable
|
|
}
|
|
|
|
#[test]
|
|
fn valuefact_widen_stable_bound() {
|
|
let mut a = ValueFact::top();
|
|
a.lo = Some(0);
|
|
a.lo_strict = true;
|
|
let mut b = ValueFact::top();
|
|
b.lo = Some(0);
|
|
b.lo_strict = true;
|
|
let w = a.widen(&b);
|
|
assert_eq!(w.lo, Some(0)); // stable, preserved
|
|
assert!(w.lo_strict);
|
|
}
|
|
|
|
// ── Nullability tests ───────────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn nullability_meet_join_exhaustive() {
|
|
use Nullability::*;
|
|
// meet: refine
|
|
assert_eq!(Unknown.meet(Null), Null);
|
|
assert_eq!(Unknown.meet(NonNull), NonNull);
|
|
assert_eq!(Null.meet(NonNull), Bottom);
|
|
assert_eq!(Null.meet(Null), Null);
|
|
assert_eq!(Bottom.meet(Unknown), Bottom);
|
|
// join: merge
|
|
assert_eq!(Null.join(NonNull), Unknown);
|
|
assert_eq!(Null.join(Null), Null);
|
|
assert_eq!(Unknown.join(Null), Unknown);
|
|
assert_eq!(Bottom.join(Null), Null);
|
|
assert_eq!(Bottom.join(Bottom), Bottom);
|
|
}
|
|
|
|
// ── BoolState tests ─────────────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn boolstate_meet_join_exhaustive() {
|
|
use BoolState::*;
|
|
assert_eq!(Unknown.meet(True), True);
|
|
assert_eq!(True.meet(False), Bottom);
|
|
assert_eq!(True.meet(True), True);
|
|
assert_eq!(Bottom.meet(True), Bottom);
|
|
assert_eq!(True.join(False), Unknown);
|
|
assert_eq!(True.join(True), True);
|
|
assert_eq!(Bottom.join(True), True);
|
|
}
|
|
|
|
// ── TypeSet tests ───────────────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn typeset_meet_is_intersection() {
|
|
use crate::ssa::type_facts::TypeKind;
|
|
let a = TypeSet::singleton(&TypeKind::String).join(TypeSet::singleton(&TypeKind::Int));
|
|
let b = TypeSet::singleton(&TypeKind::Int).join(TypeSet::singleton(&TypeKind::Bool));
|
|
let m = a.meet(b);
|
|
assert!(m.contains(&TypeKind::Int));
|
|
assert!(!m.contains(&TypeKind::String));
|
|
assert!(!m.contains(&TypeKind::Bool));
|
|
}
|
|
|
|
#[test]
|
|
fn typeset_join_is_union() {
|
|
use crate::ssa::type_facts::TypeKind;
|
|
let a = TypeSet::singleton(&TypeKind::String);
|
|
let b = TypeSet::singleton(&TypeKind::Int);
|
|
let j = a.join(b);
|
|
assert!(j.contains(&TypeKind::String));
|
|
assert!(j.contains(&TypeKind::Int));
|
|
}
|
|
|
|
#[test]
|
|
fn typeset_complement() {
|
|
use crate::ssa::type_facts::TypeKind;
|
|
let s = TypeSet::singleton(&TypeKind::String);
|
|
let c = s.complement();
|
|
assert!(!c.contains(&TypeKind::String));
|
|
assert!(c.contains(&TypeKind::Int));
|
|
assert!(c.contains(&TypeKind::Bool));
|
|
// complement of complement is original
|
|
assert_eq!(c.complement(), s);
|
|
}
|
|
|
|
#[test]
|
|
fn typeset_top_bottom() {
|
|
assert!(TypeSet::TOP.is_top());
|
|
assert!(!TypeSet::TOP.is_bottom());
|
|
assert!(TypeSet::BOTTOM.is_bottom());
|
|
assert!(!TypeSet::BOTTOM.is_top());
|
|
}
|
|
|
|
// ── PathEnv tests ───────────────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn pathenv_refine_and_get() {
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
let mut fact = ValueFact::top();
|
|
fact.null = Nullability::NonNull;
|
|
env.refine(v, &fact);
|
|
let got = env.get(v);
|
|
assert_eq!(got.null, Nullability::NonNull);
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_refine_contradiction_sets_unsat() {
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
let mut f1 = ValueFact::top();
|
|
f1.null = Nullability::Null;
|
|
env.refine(v, &f1);
|
|
assert!(!env.is_unsat());
|
|
let mut f2 = ValueFact::top();
|
|
f2.null = Nullability::NonNull;
|
|
env.refine(v, &f2);
|
|
assert!(env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_join_common_facts_preserved() {
|
|
let v = SsaValue(0);
|
|
let mut env1 = PathEnv::empty();
|
|
let mut f1 = ValueFact::top();
|
|
f1.null = Nullability::NonNull;
|
|
env1.refine(v, &f1);
|
|
let mut env2 = PathEnv::empty();
|
|
let mut f2 = ValueFact::top();
|
|
f2.null = Nullability::NonNull;
|
|
env2.refine(v, &f2);
|
|
let joined = env1.join(&env2);
|
|
let got = joined.get(v);
|
|
assert_eq!(got.null, Nullability::NonNull);
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_join_one_side_absent_drops() {
|
|
let v = SsaValue(0);
|
|
let mut env1 = PathEnv::empty();
|
|
let mut f1 = ValueFact::top();
|
|
f1.null = Nullability::NonNull;
|
|
env1.refine(v, &f1);
|
|
let env2 = PathEnv::empty(); // no fact for v
|
|
let joined = env1.join(&env2);
|
|
let got = joined.get(v);
|
|
// Intentional: absent = Top, Top.join(NonNull) = Top → dropped
|
|
assert_eq!(got.null, Nullability::Unknown);
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_join_one_side_nonnull_other_untouched() {
|
|
// Verify explicitly: one branch refines x to NonNull, other leaves x untouched
|
|
let v = SsaValue(0);
|
|
let mut env1 = PathEnv::empty();
|
|
env1.refine(v, &{
|
|
let mut f = ValueFact::top();
|
|
f.null = Nullability::NonNull;
|
|
f
|
|
});
|
|
let env2 = PathEnv::empty();
|
|
let joined = env1.join(&env2);
|
|
assert_eq!(joined.get(v).null, Nullability::Unknown); // drops to Unknown
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_join_one_side_range_other_untouched() {
|
|
let v = SsaValue(0);
|
|
let mut env1 = PathEnv::empty();
|
|
env1.refine(v, &{
|
|
let mut f = ValueFact::top();
|
|
f.lo = Some(0);
|
|
f.lo_strict = true;
|
|
f
|
|
});
|
|
let env2 = PathEnv::empty();
|
|
let joined = env1.join(&env2);
|
|
assert_eq!(joined.get(v).lo, None); // dropped
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_join_one_side_type_other_untouched() {
|
|
use crate::ssa::type_facts::TypeKind;
|
|
let v = SsaValue(0);
|
|
let mut env1 = PathEnv::empty();
|
|
env1.refine(v, &{
|
|
let mut f = ValueFact::top();
|
|
f.types = TypeSet::singleton(&TypeKind::String);
|
|
f
|
|
});
|
|
let env2 = PathEnv::empty();
|
|
let joined = env1.join(&env2);
|
|
assert!(joined.get(v).types.is_top()); // dropped to Top
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_bounded_size() {
|
|
let mut env = PathEnv::empty();
|
|
for i in 0..(MAX_PATH_ENV_ENTRIES + 10) {
|
|
let v = SsaValue(i as u32);
|
|
let mut f = ValueFact::top();
|
|
f.null = Nullability::NonNull;
|
|
env.refine(v, &f);
|
|
}
|
|
assert!(env.fact_count() <= MAX_PATH_ENV_ENTRIES);
|
|
assert!(!env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_max_refine_per_block() {
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
// Reset counter
|
|
env.reset_refine_count();
|
|
// Refine many times, should stop after MAX_REFINE_PER_BLOCK
|
|
for _ in 0..(MAX_REFINE_PER_BLOCK + 50) {
|
|
let mut f = ValueFact::top();
|
|
f.null = Nullability::NonNull;
|
|
env.refine(v, &f);
|
|
}
|
|
// Should not panic or set unsat from excessive refinement
|
|
assert!(!env.is_unsat());
|
|
}
|
|
|
|
// ── UnionFind tests ─────────────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn uf_basic_union_find() {
|
|
let mut uf = UnionFind::new();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
assert!(!uf.same_class(a, b));
|
|
uf.union(a, b);
|
|
assert!(uf.same_class(a, b));
|
|
assert_eq!(uf.find(a), uf.find(b));
|
|
}
|
|
|
|
#[test]
|
|
fn uf_transitive() {
|
|
let mut uf = UnionFind::new();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
let c = SsaValue(2);
|
|
uf.union(a, b);
|
|
uf.union(b, c);
|
|
assert!(uf.same_class(a, c));
|
|
}
|
|
|
|
#[test]
|
|
fn uf_equality_propagates_facts() {
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
env.assert_equal(a, b);
|
|
// Refine a with Eq(5) → should propagate to b
|
|
let mut fact = ValueFact::top();
|
|
fact.exact = Some(ConstValue::Int(5));
|
|
fact.lo = Some(5);
|
|
fact.hi = Some(5);
|
|
env.refine(a, &fact);
|
|
let got_b = env.get(b);
|
|
assert_eq!(got_b.exact, Some(ConstValue::Int(5)));
|
|
}
|
|
|
|
#[test]
|
|
fn uf_disequality_contradiction() {
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
env.assert_equal(a, b);
|
|
env.assert_not_equal(a, b);
|
|
assert!(env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn uf_transitive_disequality() {
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
let c = SsaValue(2);
|
|
env.assert_equal(a, b);
|
|
env.assert_equal(b, c);
|
|
// Now a==b==c, then assert a!=c → contradiction
|
|
env.assert_not_equal(a, c);
|
|
assert!(env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn uf_max_edges_bounded() {
|
|
let mut uf = UnionFind::new();
|
|
for i in 0..(MAX_EQUALITY_EDGES + 10) {
|
|
uf.union(SsaValue(0), SsaValue(i as u32 + 1));
|
|
}
|
|
assert!(uf.edge_count() <= MAX_EQUALITY_EDGES);
|
|
}
|
|
|
|
// ── Lowering tests ──────────────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn compop_flip() {
|
|
assert_eq!(CompOp::Lt.flip(), CompOp::Gt);
|
|
assert_eq!(CompOp::Gt.flip(), CompOp::Lt);
|
|
assert_eq!(CompOp::Le.flip(), CompOp::Ge);
|
|
assert_eq!(CompOp::Ge.flip(), CompOp::Le);
|
|
assert_eq!(CompOp::Eq.flip(), CompOp::Eq);
|
|
assert_eq!(CompOp::Neq.flip(), CompOp::Neq);
|
|
}
|
|
|
|
#[test]
|
|
fn compop_negate() {
|
|
assert_eq!(CompOp::Eq.negate(), CompOp::Neq);
|
|
assert_eq!(CompOp::Neq.negate(), CompOp::Eq);
|
|
assert_eq!(CompOp::Lt.negate(), CompOp::Ge);
|
|
assert_eq!(CompOp::Ge.negate(), CompOp::Lt);
|
|
assert_eq!(CompOp::Gt.negate(), CompOp::Le);
|
|
assert_eq!(CompOp::Le.negate(), CompOp::Gt);
|
|
}
|
|
|
|
#[test]
|
|
fn compop_negate_round_trip() {
|
|
for op in [
|
|
CompOp::Eq,
|
|
CompOp::Neq,
|
|
CompOp::Lt,
|
|
CompOp::Gt,
|
|
CompOp::Le,
|
|
CompOp::Ge,
|
|
] {
|
|
assert_eq!(op.negate().negate(), op);
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn condition_expr_negate_comparison() {
|
|
let expr = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(SsaValue(0)),
|
|
op: CompOp::Gt,
|
|
rhs: Operand::Const(ConstValue::Int(5)),
|
|
};
|
|
let neg = expr.negate();
|
|
match neg {
|
|
ConditionExpr::Comparison { op, .. } => assert_eq!(op, CompOp::Le),
|
|
_ => panic!("expected Comparison"),
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn condition_expr_negate_null_check() {
|
|
let expr = ConditionExpr::NullCheck {
|
|
var: SsaValue(0),
|
|
is_null: true,
|
|
};
|
|
let neg = expr.negate();
|
|
match neg {
|
|
ConditionExpr::NullCheck { is_null, .. } => assert!(!is_null),
|
|
_ => panic!("expected NullCheck"),
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn condition_expr_negate_type_check() {
|
|
let expr = ConditionExpr::TypeCheck {
|
|
var: SsaValue(0),
|
|
type_name: "number".into(),
|
|
positive: true,
|
|
};
|
|
let neg = expr.negate();
|
|
match neg {
|
|
ConditionExpr::TypeCheck { positive, .. } => assert!(!positive),
|
|
_ => panic!("expected TypeCheck"),
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn const_value_parse_literal() {
|
|
assert_eq!(ConstValue::parse_literal("5"), Some(ConstValue::Int(5)));
|
|
assert_eq!(ConstValue::parse_literal("-3"), Some(ConstValue::Int(-3)));
|
|
assert_eq!(ConstValue::parse_literal("null"), Some(ConstValue::Null));
|
|
assert_eq!(ConstValue::parse_literal("None"), Some(ConstValue::Null));
|
|
assert_eq!(
|
|
ConstValue::parse_literal("true"),
|
|
Some(ConstValue::Bool(true))
|
|
);
|
|
assert_eq!(
|
|
ConstValue::parse_literal("\"hello\""),
|
|
Some(ConstValue::Str("hello".into()))
|
|
);
|
|
assert_eq!(
|
|
ConstValue::parse_literal("'world'"),
|
|
Some(ConstValue::Str("world".into()))
|
|
);
|
|
assert_eq!(ConstValue::parse_literal(""), None);
|
|
assert_eq!(ConstValue::parse_literal("xyz"), None);
|
|
}
|
|
|
|
// ── Solver tests ────────────────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn refine_null_check_true_branch() {
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
let cond = ConditionExpr::NullCheck {
|
|
var: v,
|
|
is_null: true,
|
|
};
|
|
env = refine_env(&env, &cond, true);
|
|
assert_eq!(env.get(v).null, Nullability::Null);
|
|
}
|
|
|
|
#[test]
|
|
fn refine_null_check_false_branch() {
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
let cond = ConditionExpr::NullCheck {
|
|
var: v,
|
|
is_null: true,
|
|
};
|
|
env = refine_env(&env, &cond, false); // negated: not null
|
|
assert_eq!(env.get(v).null, Nullability::NonNull);
|
|
}
|
|
|
|
#[test]
|
|
fn refine_comparison_gt_then_lt_contradiction() {
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
// x > 10
|
|
let c1 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(v),
|
|
op: CompOp::Gt,
|
|
rhs: Operand::Const(ConstValue::Int(10)),
|
|
};
|
|
env = refine_env(&env, &c1, true);
|
|
assert!(!env.is_unsat());
|
|
// x < 5 (contradicts x > 10)
|
|
let c2 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(v),
|
|
op: CompOp::Lt,
|
|
rhs: Operand::Const(ConstValue::Int(5)),
|
|
};
|
|
env = refine_env(&env, &c2, true);
|
|
assert!(env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn refine_comparison_eq_then_neq_contradiction() {
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
let c1 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(v),
|
|
op: CompOp::Eq,
|
|
rhs: Operand::Const(ConstValue::Int(5)),
|
|
};
|
|
env = refine_env(&env, &c1, true);
|
|
assert!(!env.is_unsat());
|
|
let c2 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(v),
|
|
op: CompOp::Neq,
|
|
rhs: Operand::Const(ConstValue::Int(5)),
|
|
};
|
|
env = refine_env(&env, &c2, true);
|
|
assert!(env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn refine_comparison_eq_string_then_different_string() {
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
let c1 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(v),
|
|
op: CompOp::Eq,
|
|
rhs: Operand::Const(ConstValue::Str("safe".into())),
|
|
};
|
|
env = refine_env(&env, &c1, true);
|
|
let c2 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(v),
|
|
op: CompOp::Eq,
|
|
rhs: Operand::Const(ConstValue::Str("dangerous".into())),
|
|
};
|
|
env = refine_env(&env, &c2, true);
|
|
assert!(
|
|
env.is_unsat(),
|
|
"Eq('safe') ∧ Eq('dangerous') should be unsat"
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn refine_type_check_positive() {
|
|
use crate::ssa::type_facts::TypeKind;
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
let cond = ConditionExpr::TypeCheck {
|
|
var: v,
|
|
type_name: "number".into(),
|
|
positive: true,
|
|
};
|
|
env = refine_env(&env, &cond, true);
|
|
let got = env.get(v);
|
|
assert!(got.types.contains(&TypeKind::Int));
|
|
assert!(!got.types.contains(&TypeKind::String));
|
|
assert_eq!(got.null, Nullability::NonNull);
|
|
}
|
|
|
|
#[test]
|
|
fn refine_type_check_negative() {
|
|
use crate::ssa::type_facts::TypeKind;
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
let cond = ConditionExpr::TypeCheck {
|
|
var: v,
|
|
type_name: "number".into(),
|
|
positive: true,
|
|
};
|
|
env = refine_env(&env, &cond, false); // NOT number
|
|
let got = env.get(v);
|
|
assert!(!got.types.contains(&TypeKind::Int));
|
|
assert!(got.types.contains(&TypeKind::String));
|
|
}
|
|
|
|
#[test]
|
|
fn refine_value_eq_value() {
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
// First: a is NonNull
|
|
env.refine(a, &{
|
|
let mut f = ValueFact::top();
|
|
f.null = Nullability::NonNull;
|
|
f
|
|
});
|
|
// Then: a == b → b should also become NonNull
|
|
let cond = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(a),
|
|
op: CompOp::Eq,
|
|
rhs: Operand::Value(b),
|
|
};
|
|
env = refine_env(&env, &cond, true);
|
|
assert_eq!(env.get(b).null, Nullability::NonNull);
|
|
}
|
|
|
|
#[test]
|
|
fn refine_unknown_is_noop() {
|
|
let env = PathEnv::empty();
|
|
let refined = refine_env(&env, &ConditionExpr::Unknown, true);
|
|
assert!(!refined.is_unsat());
|
|
assert_eq!(refined.fact_count(), 0);
|
|
}
|
|
|
|
#[test]
|
|
fn refine_booltest_conservative() {
|
|
// BoolTest should NOT add NonNull for non-boolean-typed values
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
let cond = ConditionExpr::BoolTest { var: v };
|
|
env = refine_env(&env, &cond, true);
|
|
// Since v has no known type, BoolTest should be conservative
|
|
assert_eq!(env.get(v).null, Nullability::Unknown);
|
|
}
|
|
|
|
#[test]
|
|
fn refine_booltest_boolean_typed() {
|
|
use crate::ssa::type_facts::TypeKind;
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
// First: mark v as boolean-typed
|
|
env.refine(v, &{
|
|
let mut f = ValueFact::top();
|
|
f.types = TypeSet::singleton(&TypeKind::Bool);
|
|
f
|
|
});
|
|
// Now BoolTest should refine to True + NonNull
|
|
let cond = ConditionExpr::BoolTest { var: v };
|
|
env = refine_env(&env, &cond, true);
|
|
assert_eq!(env.get(v).bool_state, BoolState::True);
|
|
assert_eq!(env.get(v).null, Nullability::NonNull);
|
|
}
|
|
|
|
#[test]
|
|
fn refine_comparison_feasible_range_not_pruned() {
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
// x > 0
|
|
let c1 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(v),
|
|
op: CompOp::Gt,
|
|
rhs: Operand::Const(ConstValue::Int(0)),
|
|
};
|
|
env = refine_env(&env, &c1, true);
|
|
// x < 100 (compatible with x > 0)
|
|
let c2 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(v),
|
|
op: CompOp::Lt,
|
|
rhs: Operand::Const(ConstValue::Int(100)),
|
|
};
|
|
env = refine_env(&env, &c2, true);
|
|
assert!(
|
|
!env.is_unsat(),
|
|
"feasible range (0, 100) should not be pruned"
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn refine_null_then_eq_string_contradiction() {
|
|
let mut env = PathEnv::empty();
|
|
let v = SsaValue(0);
|
|
// x is null
|
|
let c1 = ConditionExpr::NullCheck {
|
|
var: v,
|
|
is_null: true,
|
|
};
|
|
env = refine_env(&env, &c1, true);
|
|
// x == "rm" (contradicts: null value can't be a string)
|
|
let c2 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(v),
|
|
op: CompOp::Eq,
|
|
rhs: Operand::Const(ConstValue::Str("rm".into())),
|
|
};
|
|
env = refine_env(&env, &c2, true);
|
|
assert!(env.is_unsat(), "null ∧ Eq('rm') should be unsat");
|
|
}
|
|
|
|
// ── parse_type_name tests ───────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn parse_type_name_coverage() {
|
|
use crate::ssa::type_facts::TypeKind;
|
|
assert_eq!(parse_type_name("string"), Some(TypeKind::String));
|
|
assert_eq!(parse_type_name("str"), Some(TypeKind::String));
|
|
assert_eq!(parse_type_name("number"), Some(TypeKind::Int));
|
|
assert_eq!(parse_type_name("int"), Some(TypeKind::Int));
|
|
assert_eq!(parse_type_name("boolean"), Some(TypeKind::Bool));
|
|
assert_eq!(parse_type_name("bool"), Some(TypeKind::Bool));
|
|
assert_eq!(parse_type_name("object"), Some(TypeKind::Object));
|
|
assert_eq!(parse_type_name("array"), Some(TypeKind::Array));
|
|
assert_eq!(parse_type_name("null"), Some(TypeKind::Null));
|
|
assert_eq!(parse_type_name("undefined"), Some(TypeKind::Null));
|
|
assert_eq!(parse_type_name("blah"), None);
|
|
}
|
|
|
|
// ── PathEnv seed tests ──────────────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn pathenv_seed_from_optimization() {
|
|
use crate::ssa::type_facts::{TypeFact, TypeFactResult, TypeKind};
|
|
let mut env = PathEnv::empty();
|
|
let v0 = SsaValue(0);
|
|
let v1 = SsaValue(1);
|
|
let mut const_values = HashMap::new();
|
|
const_values.insert(v0, ConstLattice::Int(42));
|
|
let mut type_facts = TypeFactResult {
|
|
facts: HashMap::new(),
|
|
};
|
|
type_facts.facts.insert(
|
|
v1,
|
|
TypeFact {
|
|
kind: TypeKind::String,
|
|
nullable: false,
|
|
},
|
|
);
|
|
env.seed_from_optimization(&const_values, &type_facts);
|
|
let f0 = env.get(v0);
|
|
assert_eq!(f0.exact, Some(ConstValue::Int(42)));
|
|
assert_eq!(f0.null, Nullability::NonNull);
|
|
let f1 = env.get(v1);
|
|
assert!(f1.types.contains(&TypeKind::String));
|
|
assert_eq!(f1.null, Nullability::NonNull);
|
|
}
|
|
|
|
// ── Relational constraint tests ────────────────────────────────────────
|
|
|
|
#[test]
|
|
fn pathenv_relational_lt_lt_contradiction() {
|
|
// a < b then b < a → unsat (both strict)
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
env.assert_relational(a, RelOp::Lt, b);
|
|
assert!(!env.is_unsat());
|
|
env.assert_relational(b, RelOp::Lt, a);
|
|
assert!(env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_lt_le_contradiction() {
|
|
// a < b then b <= a → unsat (one strict suffices)
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
env.assert_relational(a, RelOp::Lt, b);
|
|
assert!(!env.is_unsat());
|
|
env.assert_relational(b, RelOp::Le, a);
|
|
assert!(env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_le_lt_contradiction() {
|
|
// a <= b then b < a → unsat (symmetric)
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
env.assert_relational(a, RelOp::Le, b);
|
|
assert!(!env.is_unsat());
|
|
env.assert_relational(b, RelOp::Lt, a);
|
|
assert!(env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_le_le_not_contradiction() {
|
|
// a <= b then b <= a → NOT unsat (a == b is satisfiable)
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
env.assert_relational(a, RelOp::Le, b);
|
|
assert!(!env.is_unsat());
|
|
env.assert_relational(b, RelOp::Le, a);
|
|
assert!(!env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_transitive_cycle() {
|
|
// a < b, b < c, c < a → unsat (cycle with strict edge)
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
let c = SsaValue(2);
|
|
env.assert_relational(a, RelOp::Lt, b);
|
|
assert!(!env.is_unsat());
|
|
env.assert_relational(b, RelOp::Lt, c);
|
|
assert!(!env.is_unsat());
|
|
env.assert_relational(c, RelOp::Lt, a);
|
|
assert!(env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_transitive_all_le_cycle() {
|
|
// a <= b, b <= c, c <= a → NOT unsat (all equal is satisfiable)
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
let c = SsaValue(2);
|
|
env.assert_relational(a, RelOp::Le, b);
|
|
env.assert_relational(b, RelOp::Le, c);
|
|
env.assert_relational(c, RelOp::Le, a);
|
|
assert!(!env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_cross_interval_refine_strict() {
|
|
// a < b with b ∈ [0, 10] → a.hi = 9 (strict: h-1)
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
let mut b_fact = ValueFact::top();
|
|
b_fact.lo = Some(0);
|
|
b_fact.hi = Some(10);
|
|
env.refine(b, &b_fact);
|
|
env.assert_relational(a, RelOp::Lt, b);
|
|
let fa = env.get(a);
|
|
assert_eq!(fa.hi, Some(9));
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_cross_interval_refine_nonstrict() {
|
|
// a <= b with b ∈ [0, 10] → a.hi = 10 (non-strict)
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
let mut b_fact = ValueFact::top();
|
|
b_fact.lo = Some(0);
|
|
b_fact.hi = Some(10);
|
|
env.refine(b, &b_fact);
|
|
env.assert_relational(a, RelOp::Le, b);
|
|
let fa = env.get(a);
|
|
assert_eq!(fa.hi, Some(10));
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_cross_interval_refine_reverse() {
|
|
// a < b with a ∈ [5, 20] → b.lo = 6 (strict: l+1)
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
let mut a_fact = ValueFact::top();
|
|
a_fact.lo = Some(5);
|
|
a_fact.hi = Some(20);
|
|
env.refine(a, &a_fact);
|
|
env.assert_relational(a, RelOp::Lt, b);
|
|
let fb = env.get(b);
|
|
assert_eq!(fb.lo, Some(6));
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_join_intersection() {
|
|
// Only shared constraints survive join
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
let c = SsaValue(2);
|
|
|
|
let mut env1 = PathEnv::empty();
|
|
env1.assert_relational(a, RelOp::Lt, b);
|
|
env1.assert_relational(b, RelOp::Lt, c);
|
|
|
|
let mut env2 = PathEnv::empty();
|
|
env2.assert_relational(a, RelOp::Lt, b);
|
|
// env2 does NOT have b < c
|
|
|
|
let joined = env1.join(&env2);
|
|
assert!(!joined.is_unsat());
|
|
// The shared constraint a < b should survive;
|
|
// b < c should be lost. We can verify by adding c < a
|
|
// which would be contradictory with both a < b and b < c,
|
|
// but only the first matters here.
|
|
// (We can't directly inspect relational, but we can test behavior)
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_max_bounded() {
|
|
// Exceeding MAX_RELATIONAL doesn't panic
|
|
let mut env = PathEnv::empty();
|
|
for i in 0..MAX_RELATIONAL + 5 {
|
|
let a = SsaValue(i as u32 * 2);
|
|
let b = SsaValue(i as u32 * 2 + 1);
|
|
env.assert_relational(a, RelOp::Lt, b);
|
|
assert!(!env.is_unsat());
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_eq_then_strict_lt() {
|
|
// assert_equal(a, b) then a < b → unsat
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
env.assert_relational(a, RelOp::Lt, b);
|
|
assert!(!env.is_unsat());
|
|
env.assert_equal(a, b);
|
|
assert!(env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_eq_then_le_ok() {
|
|
// assert_equal(a, b) then a <= b is fine (Le compat with equality)
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
env.assert_relational(a, RelOp::Le, b);
|
|
assert!(!env.is_unsat());
|
|
env.assert_equal(a, b);
|
|
assert!(!env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn solver_value_lt_value() {
|
|
// End-to-end via refine_env with Comparison { Value(a), Lt, Value(b) }
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
let env = PathEnv::empty();
|
|
|
|
// True branch: a < b holds
|
|
let cond = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(a),
|
|
op: CompOp::Lt,
|
|
rhs: Operand::Value(b),
|
|
};
|
|
let true_env = refine_env(&env, &cond, true);
|
|
assert!(!true_env.is_unsat());
|
|
|
|
// Now on true branch, assert b < a → should be unsat
|
|
let cond2 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(b),
|
|
op: CompOp::Lt,
|
|
rhs: Operand::Value(a),
|
|
};
|
|
let nested = refine_env(&true_env, &cond2, true);
|
|
assert!(nested.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn solver_value_gt_value_contradiction() {
|
|
// a > b on true branch, then b > a → unsat (via Gt → Lt flip)
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
let env = PathEnv::empty();
|
|
|
|
let cond1 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(a),
|
|
op: CompOp::Gt,
|
|
rhs: Operand::Value(b),
|
|
};
|
|
let env1 = refine_env(&env, &cond1, true);
|
|
assert!(!env1.is_unsat());
|
|
|
|
let cond2 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(b),
|
|
op: CompOp::Gt,
|
|
rhs: Operand::Value(a),
|
|
};
|
|
let env2 = refine_env(&env1, &cond2, true);
|
|
assert!(env2.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn solver_value_le_ge_not_contradiction() {
|
|
// a <= b then a >= b (i.e. b <= a) → NOT unsat (a == b)
|
|
let a = SsaValue(0);
|
|
let b = SsaValue(1);
|
|
let env = PathEnv::empty();
|
|
|
|
let cond1 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(a),
|
|
op: CompOp::Le,
|
|
rhs: Operand::Value(b),
|
|
};
|
|
let env1 = refine_env(&env, &cond1, true);
|
|
assert!(!env1.is_unsat());
|
|
|
|
let cond2 = ConditionExpr::Comparison {
|
|
lhs: Operand::Value(a),
|
|
op: CompOp::Ge,
|
|
rhs: Operand::Value(b),
|
|
};
|
|
let env2 = refine_env(&env1, &cond2, true);
|
|
assert!(!env2.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_self_lt_unsat() {
|
|
// a < a → unsat immediately
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
env.assert_relational(a, RelOp::Lt, a);
|
|
assert!(env.is_unsat());
|
|
}
|
|
|
|
#[test]
|
|
fn pathenv_relational_self_le_ok() {
|
|
// a <= a → trivially true, not unsat
|
|
let mut env = PathEnv::empty();
|
|
let a = SsaValue(0);
|
|
env.assert_relational(a, RelOp::Le, a);
|
|
assert!(!env.is_unsat());
|
|
}
|