mirror of
https://github.com/norandom/OpenUltraSAST.git
synced 2026-11-13 17:58:18 +00:00
155 lines
5.6 KiB
Python
155 lines
5.6 KiB
Python
"""Task 10.4 -- one judgment per path (Reqs 4.1-4.3, 11.2-11.4).
|
|||
|
|
|
||
|
|
Fixtures build WitnessMatch and DominanceEvidence directly; the truth table
|
||
|
|
pinned here is the design's: a witness governs only when every dimension is
|
||
|
|
MUST; one definite NO with the rest definite makes the path unguarded; any
|
||
|
|
MAY or UNKNOWN among required relations makes it indeterminate.
|
||
|
|
"""
|
||
|
|
|
||
|
|
import pytest
|
||
|
|
|
||
|
|
from openultrasast.semantic.obligations.abstract_domain import (
|
||
|
|
Completeness,
|
||
|
|
EvidenceRelation,
|
||
|
|
PairJudgment,
|
||
|
|
WitnessMatch,
|
||
|
|
)
|
||
|
|
from openultrasast.semantic.obligations.cfg_dominance import DominanceEvidence
|
||
|
|
from openultrasast.semantic.obligations.judgment import judgment_for_path
|
||
|
|
from openultrasast.semantic.obligations.operations import Operation
|
||
|
|
|
||
|
|
PATH = "src/C.java"
|
||
|
|
|
||
|
|
|
||
|
|
def _operation() -> Operation:
|
||
|
|
return Operation(PATH, 4, "handle", "protected_read", "f:op", "book", ("path_guard", "ownership_check"))
|
||
|
|
|
||
|
|
|
||
|
|
def _match(relation: EvidenceRelation) -> WitnessMatch:
|
||
|
|
return WitnessMatch(
|
||
|
|
relation=relation,
|
||
|
|
resource_relation=EvidenceRelation.MUST,
|
||
|
|
authority_relation=EvidenceRelation.MUST,
|
||
|
|
evidence=("witness:f:guard", "operation:f:op"),
|
||
|
|
)
|
||
|
|
|
||
|
|
|
||
|
|
def _dominance(relation: EvidenceRelation) -> DominanceEvidence:
|
||
|
|
return DominanceEvidence(relation=relation, guard_effect="throws")
|
||
|
|
|
||
|
|
|
||
|
|
def _complete() -> Completeness:
|
||
|
|
return Completeness(is_complete=True)
|
||
|
|
|
||
|
|
|
||
|
|
def _matches_by_kind(
|
||
|
|
path_guard: tuple[tuple[WitnessMatch, DominanceEvidence], ...],
|
||
|
|
ownership_check: tuple[tuple[WitnessMatch, DominanceEvidence], ...],
|
||
|
|
) -> dict[str, tuple[tuple[WitnessMatch, DominanceEvidence], ...]]:
|
||
|
|
return {"path_guard": path_guard, "ownership_check": ownership_check}
|
||
|
|
|
||
|
|
|
||
|
|
def test_must_and_no_produce_unguarded_with_missing_kind() -> None:
|
||
|
|
judgment = judgment_for_path(
|
||
|
|
_operation(),
|
||
|
|
_matches_by_kind(((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),), ()),
|
||
|
|
_complete(),
|
||
|
|
)
|
||
|
|
assert judgment.judgment is PairJudgment.UNGUARDED
|
||
|
|
assert judgment.missing == ("ownership_check",)
|
||
|
|
|
||
|
|
|
||
|
|
def test_all_must_produces_discharged() -> None:
|
||
|
|
pairs = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),)
|
||
|
|
judgment = judgment_for_path(_operation(), _matches_by_kind(pairs, pairs), _complete())
|
||
|
|
assert judgment.judgment is PairJudgment.DISCHARGED
|
||
|
|
assert judgment.missing == ()
|
||
|
|
|
||
|
|
|
||
|
|
def test_may_and_no_produce_indeterminate() -> None:
|
||
|
|
judgment = judgment_for_path(
|
||
|
|
_operation(),
|
||
|
|
_matches_by_kind(
|
||
|
|
((_match(EvidenceRelation.MAY), _dominance(EvidenceRelation.MUST)),),
|
||
|
|
(),
|
||
|
|
),
|
||
|
|
_complete(),
|
||
|
|
)
|
||
|
|
assert judgment.judgment is PairJudgment.INDETERMINATE
|
||
|
|
|
||
|
|
|
||
|
|
def test_unknown_match_relation_produces_indeterminate() -> None:
|
||
|
|
judgment = judgment_for_path(
|
||
|
|
_operation(),
|
||
|
|
_matches_by_kind(
|
||
|
|
((_match(EvidenceRelation.UNKNOWN), _dominance(EvidenceRelation.MUST)),),
|
||
|
|
(),
|
||
|
|
),
|
||
|
|
_complete(),
|
||
|
|
)
|
||
|
|
assert judgment.judgment is PairJudgment.INDETERMINATE
|
||
|
|
|
||
|
|
|
||
|
|
def test_unknown_dominance_produces_indeterminate() -> None:
|
||
|
|
judgment = judgment_for_path(
|
||
|
|
_operation(),
|
||
|
|
_matches_by_kind(
|
||
|
|
((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.UNKNOWN)),),
|
||
|
|
(),
|
||
|
|
),
|
||
|
|
_complete(),
|
||
|
|
)
|
||
|
|
assert judgment.judgment is PairJudgment.INDETERMINATE
|
||
|
|
|
||
|
|
|
||
|
|
def test_empty_witnesses_with_complete_discovery_are_unguarded() -> None:
|
||
|
|
judgment = judgment_for_path(_operation(), _matches_by_kind((), ()), _complete())
|
||
|
|
assert judgment.judgment is PairJudgment.UNGUARDED
|
||
|
|
assert judgment.missing == ("ownership_check", "path_guard")
|
||
|
|
|
||
|
|
|
||
|
|
def test_empty_witnesses_without_discovery_are_indeterminate() -> None:
|
||
|
|
judgment = judgment_for_path(_operation(), _matches_by_kind((), ()), _complete(), discovery_complete=False)
|
||
|
|
assert judgment.judgment is PairJudgment.INDETERMINATE
|
||
|
|
|
||
|
|
|
||
|
|
def test_incomplete_path_completeness_is_indeterminate() -> None:
|
||
|
|
pairs = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),)
|
||
|
|
judgment = judgment_for_path(
|
||
|
|
_operation(),
|
||
|
|
_matches_by_kind(pairs, pairs),
|
||
|
|
Completeness(is_complete=False, reasons=("resolution:no_candidate",)),
|
||
|
|
)
|
||
|
|
assert judgment.judgment is PairJudgment.INDETERMINATE
|
||
|
|
|
||
|
|
|
||
|
|
def test_matches_are_carried_in_the_judgment() -> None:
|
||
|
|
must_pair = (_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST))
|
||
|
|
judgment = judgment_for_path(_operation(), _matches_by_kind((must_pair,), (must_pair,)), _complete())
|
||
|
|
assert judgment.matches == (_match(EvidenceRelation.MUST),)
|
||
|
|
assert judgment.matches[0].evidence == ("witness:f:guard", "operation:f:op")
|
||
|
|
|
||
|
|
|
||
|
|
def test_judgment_is_deterministic() -> None:
|
||
|
|
pairs = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),)
|
||
|
|
first = judgment_for_path(_operation(), _matches_by_kind(pairs, ()), _complete())
|
||
|
|
second = judgment_for_path(_operation(), _matches_by_kind(pairs, ()), _complete())
|
||
|
|
assert first == second
|
||
|
|
|
||
|
|
|
||
|
|
def test_empty_requires_with_no_witnesses_is_discharged() -> None:
|
||
|
|
operation = Operation(PATH, 4, "handle", "protected_read", "f:op", "book", ())
|
||
|
|
judgment = judgment_for_path(operation, {}, _complete())
|
||
|
|
assert judgment.judgment is PairJudgment.DISCHARGED
|
||
|
|
|
||
|
|
|
||
|
|
def test_no_witness_for_one_kind_only_reports_that_kind() -> None:
|
||
|
|
must_pair = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),)
|
||
|
|
judgment = judgment_for_path(_operation(), _matches_by_kind(must_pair, ()), _complete())
|
||
|
|
assert judgment.judgment is PairJudgment.UNGUARDED
|
||
|
|
assert judgment.missing == ("ownership_check",)
|
||
|
|
|
||
|
|
|
||
|
|
if __name__ == "__main__": # pragma: no cover
|
||
|
|
pytest.main([__file__, "-q"])
|