Skip to main content

Module functions

oxilean_std::static_analysis

Module functions 

Source
Expand description

Auto-generated module

πŸ€– Generated with SplitRS

Functions§

abstract_closure_ty
AbstractClosure : Type β€” An abstract closure: (lambda, env).
abstract_interp_sound_ty
AbstractInterp_Sound : βˆ€ prog, Ξ±(collect prog) βŠ‘ abs_semantics prog
abstract_semantics_ty
AbstractSemantics : Program β†’ AbsDom β€” Abstract semantics over an abstract domain.
abstraction_ty
Abstraction : ConcreteSemantics β†’ AbsDom β€” Abstraction function Ξ±.
affine_type_ty
AffineType : ResourceType β†’ Prop β€” Resource used at most once.
algebraic_effect_handler_ty
AlgebraicEffectHandler : EffectSet β†’ Type β†’ Type Handler type that handles a set of algebraic effects.
alias_result_ty
AliasResult : Var β†’ Var β†’ Prop β€” Two variables may alias.
alias_undecidable_ty
Alias_Undecidable : alias analysis is undecidable in general
alloc_site_ty
AllocSite : Type β€” An allocation site (abstract heap location).
andersen_analysis_ty
AndersenAnalysis : Program β†’ PointsTo β€” Andersen inclusion-based pointer analysis.
andersen_cubic_ty
Andersen_Cubic : Andersen analysis is O(nΒ³) in the worst case
andersen_sound_ty
Andersen_Sound : βˆ€ prog, andersen is a sound over-approximation
app
app2
app3
arrow
atomic_block_ty
AtomicBlock : Program β†’ Stmt β†’ Prop A statement executes atomically with respect to all other threads.
atomicity_serializability_ty
Atomicity_Serializability : βˆ€ prog s, Atomic prog s β†’ serializable_execution prog s
backward_slice_ty
BackwardSlice : PDG β†’ SliceCriterion β†’ Set Stmt Backward slice: all statements that can affect the criterion.
bitfield_domain_ty
BitfieldDomain : Type β€” Abstract domain tracking known/unknown bits.
blame_theorem_ty
Blame_Theorem : dynamic cast failures are attributed to correct source location
bool_ty
borrow_check_mem_safe_ty
BorrowCheck_MemSafe : βˆ€ prog, borrow_check prog β†’ memory_safe prog
borrow_check_ty
BorrowCheck : Program β†’ Prop β€” Rust-like borrow checker soundness.
borrow_kind_ty
BorrowKind : Type β€” Borrow flavor: immutable (&) or mutable (&mut).
build_static_analysis_env
Populate an OxiLean kernel Environment with all static-analysis axioms.
bvar
call_site_ty
CallSite : Type β€” A call site in the program.
capability_judgment_ty
CapabilityJudgment : Context β†’ Expr β†’ EffectType β†’ Prop Typing judgment: in context Ξ“ with capabilities C, expression e has effect type T.
capability_set_ty
CapabilitySet : Type β€” A set of capabilities (permissions) held at a program point.
cast_correctness_ty
CastCorrectness : βˆ€ e, eval (cast_insert e) = gradual_eval e Cast insertion preserves semantics.
cast_insertion_ty
CastInsertion : GradualExpr β†’ StaticExpr β€” Elaborates gradual to casted static code.
cfa_monotone_k_ty
CFA_Monotone_in_k : 0-CFA βŠ‘ 1-CFA βŠ‘ 2-CFA βŠ‘ …
cfa_overapprox_ty
CFA_Overapprox : βˆ€ k prog, k_cfa k prog βŠ‡ actual call targets
complete_lattice_galois_ty
CompleteLattice_GaloisConnection : every Galois connection yields a complete lattice
concrete_semantics_ty
ConcreteSemantics : Program β†’ Set State β€” Collecting semantics.
concretization_ty
Concretization : AbsDom β†’ ConcreteSemantics β€” Concretization function Ξ³.
consistency_rel_ty
ConsistencyRel : GradualType β†’ GradualType β†’ Prop β€” Type consistency (~).
const_fold_correct_ty
ConstFold_Correct : βˆ€ e, eval (const_fold e) = eval e
constant_folding_ty
ConstantFolding : Expr β†’ Expr β€” Evaluate constant sub-expressions at compile time.
constant_propagation_ty
ConstantPropagation : Program β†’ Var β†’ Option Val Statically determine the value of a variable if it is constant.
control_dependence_ty
ControlDependence : Stmt β†’ Stmt β†’ Prop β€” Control dependence edge.
cst
cyclic_pred_ty
CyclicPred : HeapGraph β†’ HeapNode β†’ Prop A node may be part of a cyclic structure.
data_dependence_ty
DataDependence : Stmt β†’ Stmt β†’ Prop β€” def-use data dependence edge.
data_race_freedom_ty
DataRaceFreedom : Program β†’ Prop β€” No data races in the program.
data_race_ty
DataRace : Event β†’ Event β†’ Prop Two events form a data race if they access the same location, at least one is a write, they are from different threads, and not ordered by HB.
deadlock_freedom_ty
DeadlockFreedom : Program β†’ Prop β€” No circular lock dependencies.
declassification_ty
Declassification : Expr β†’ SecurityLabel β†’ SecurityLabel β†’ Prop Explicit declassification from high to low label.
definite_assignment_ty
DefiniteAssignment : Program β†’ Var β†’ Prop Every use of a variable is preceded by a definition.
drf_sequential_ty
DRF_Sequential : βˆ€ prog, DRF prog β†’ sequential_consistent prog
effect_polymorphism_ty
EffectPolymorphism : βˆ€ e f, e : T!{f} β†’ e : T!{f βˆͺ g} β€” Effect weakening.
effect_set_ty
EffectSet : Type β€” A set of effects annotating an expression or function.
effect_sound_ty
EffectSound : βˆ€ prog, infer_effects prog βŠ‡ actual_effects prog
effect_subtype_ty
EffectSubtype : EffectType β†’ EffectType β†’ Prop β€” Subtyping with effects.
effect_ty
Effect : Type β€” An abstract program effect (read, write, alloc, throw, io).
effect_type_ty
EffectType : Type β†’ EffectSet β†’ Type β€” A type annotated with an effect.
eraser_invariant_ty
Eraser_Invariant : C(v) β‰  βˆ… β†’ no data race on v
eraser_lock_set_ty
EraserLockSet : Thread β†’ MemLoc β†’ Set Lock Eraser algorithm: track C(v) = intersection of lock sets for variable v.
escape_analysis_ty
EscapeAnalysis : Program β†’ Var β†’ Bool Returns true if a variable’s value may escape its defining scope.
escape_sound_ty
Escape_Sound : βˆ€ prog v, Β¬escape prog v β†’ stack_allocated prog v
exn_effect_ty
ExnEffect : ExnType β†’ Effect β€” Raising an exception.
forward_slice_ty
ForwardSlice : PDG β†’ SliceCriterion β†’ Set Stmt Forward slice: all statements that the criterion can affect.
frame_rule_ty
FrameRule : βˆ€ prog P Q R, {P} prog {Q} β†’ {P * R} prog {Q * R} β€” Frame rule.
galois_connection_ty
GaloisConnection : (C β†’ A) Γ— (A β†’ C) β†’ Prop (Ξ±, Ξ³) form a Galois connection: Ξ±(c) βŠ‘ a ↔ c βŠ† Ξ³(a).
galois_insertion_ty
GaloisInsertion : GaloisConnection β†’ Prop β€” α∘γ = id (optimal abstraction).
graded_monad_ty
GradedMonad : (EffectSet β†’ Type β†’ Type) β†’ Prop A graded monad indexed by effect sets.
gradual_type_ty
GradualType : Type β€” A gradual type (may contain the unknown type ?).
happens_before_ty
HappensBefore : Event β†’ Event β†’ Prop β€” The happens-before partial order.
heap_graph_ty
HeapGraph : Type β€” A shape graph: nodes are abstract heap cells.
heap_node_ty
HeapNode : Type β€” An abstract heap node (summary or concrete).
heap_shape_tree_pred_ty
HeapShape_TreePred : HeapNode β†’ SepPred β€” Predicate for an acyclic linked list.
ifc_type_system_ty
IFCTypeSystem : Context β†’ Expr β†’ LabeledType β†’ Prop Information flow control typing judgment.
infer_effects_ty
infer_effects : Program β†’ EffectMap β€” Effect inference over a whole program.
interval_domain_ty
IntervalDomain : Type β€” Abstract domain for value range analysis (intervals).
k_cfa_complexity_ty
KCFA_Complexity : k-CFA is EXPTIME-complete for k β‰₯ 1
k_cfa_ty
KCFA : Nat β†’ Program β†’ (CallSite Γ— List CallSite) β†’ Set AbstractClosure k-CFA: context-sensitive with call-string depth k.
label_env_ty
LabelEnv : Var β†’ SecurityLabel β€” Security label environment.
lattice_bottom_ty
LatticeBottom : βˆ€ L, Lattice L β†’ L β€” Bottom element βŠ₯.
lattice_join_ty
LatticeJoin : βˆ€ L, Lattice L β†’ L β†’ L β†’ L β€” Join operator βŠ”.
lattice_leq_ty
LatticeLeq : βˆ€ L, Lattice L β†’ L β†’ L β†’ Prop β€” Partial order βŠ‘.
lattice_meet_ty
LatticeMeet : βˆ€ L, Lattice L β†’ L β†’ L β†’ L β€” Meet operator βŠ“.
lattice_top_ty
LatticeTop : βˆ€ L, Lattice L β†’ L β€” Top element ⊀.
lattice_ty
Lattice : Type β†’ Type β€” A complete lattice on a carrier type.
leak_freedom_ty
LeakFreedom : Program β†’ Prop β€” All acquired resources are released.
lifetime_subtyping_ty
LifetimeSubtyping : Lifetime β†’ Lifetime β†’ Prop β€” ’a: ’b (a outlives b).
lifetime_ty
Lifetime : Type β€” A lifetime region for borrow validity.
linear_type_leak_free_ty
LinearType_LeakFree : βˆ€ prog, well_typed_linear prog β†’ LeakFreedom prog
linear_type_ty
LinearType : ResourceType β†’ Prop β€” Resource must be used exactly once.
liquid_haskell_sound_ty
Liquid_Haskell_Sound : βˆ€ prog, liquid_type_check prog β†’ no_runtime_type_errors prog
liquid_type_complete_ty
LiquidType_Complete : liquid type inference is complete for the qualifier set
liquid_type_ty
LiquidType : BaseType β†’ Qualifier β†’ RefinementType A liquid type {v : B | Q(v)} with a qualifier drawn from a template set.
list_ty
lock_order_acyclic_ty
LockOrder_Acyclic : βˆ€ prog, acyclic_lock_order prog β†’ DeadlockFreedom prog
lock_order_ty
LockOrder : Lock β†’ Lock β†’ Prop β€” A consistent lock acquisition order.
lock_set_analysis_ty
LockSetAnalysis : Program β†’ Thread β†’ MemLoc β†’ LockSet Compute the set of locks held by thread t when accessing loc.
lock_set_ty
LockSet : Type β€” The set of locks held by a thread.
may_alias_ty
MayAlias : Program β†’ Var β†’ Var β†’ Bool
memory_safety_ty
MemorySafety : Program β†’ SepPred β†’ Prop β€” No out-of-bounds or dangling access.
monadic_effect_ty
MonadicEffect : Type β†’ EffectSet β†’ Type A computation of type T with effects E (monadic encoding).
moore_family_ty
MooreFamily : Set (Set A) β†’ Prop β€” Closed under arbitrary intersection.
must_alias_pair_ty
MustAliasPair : Program β†’ Var β†’ Var β†’ Bool
must_alias_ty
MustAlias : HeapGraph β†’ HeapNode β†’ HeapNode β†’ ThreeValued
must_use_resource_ty
MustUseResource : Typestate β†’ Prop β€” Resource in this state must be consumed.
narrowing_refines_post_ty
Narrowing_RefinesPost : βˆ€ x y, y βŠ‘ x β†’ y β–³ (f x) βŠ‘ x
narrowing_ty
Narrowing : AbsDom β†’ AbsDom β†’ AbsDom β€” Narrowing operator β–³.
nat_ty
ni_theorem_ty
NI_Theorem : βˆ€ prog env, IFC_typed prog env β†’ NonInterference prog env
no_alias_ty
NoAlias : Var β†’ Var β†’ Prop β€” Two variables definitely do not alias.
non_interference_ty
NonInterference : Program β†’ LabelEnv β†’ Prop Low-equivalent inputs produce low-equivalent outputs.
non_lexical_lifetime_ty
NonLexicalLifetime : Program β†’ LifetimeAnnotation Non-lexical lifetime inference for precise scope analysis.
null_analysis_sound_ty
NullAnalysis_Sound : βˆ€ prog, null_pointer_analysis is sound
null_pointer_analysis_ty
NullPointerAnalysis : Program β†’ Var β†’ ThreeValued Three-valued result: definitely null / definitely non-null / maybe null.
null_safety_ty
NullSafety : Program β†’ Prop β€” No null dereferences occur.
nullability_annotation_ty
NullabilityAnnotation : Type β†’ Bool β†’ Type Type annotated with nullability: T? vs T!.
option_ty
ownership_transfer_ty
OwnershipTransfer : SepPred β†’ SepPred β†’ Prop Ownership transfer from pre to post (move semantics).
ownership_type_ty
OwnershipType : Type β€” A type carrying ownership (unique, shared, borrowed).
ownership_unique_ty
OwnershipUnique : OwnershipType β†’ Prop β€” At most one owner at any time.
pair_ty
pi
points_to_cell_ty
PointsToCell : Addr β†’ Val β†’ SepPred β€” Singleton heap cell l ↦ v.
points_to_ty
PointsTo : Var β†’ Set AllocSite β€” Points-to set for a variable.
program_dependence_graph_ty
ProgramDependenceGraph : Program β†’ PDG Build the program dependence graph combining data and control edges.
prop
pure_function_ty
PureFunction : Expr β†’ Prop β€” A function with empty effect set.
qualifier_instantiation_ty
QualifierInstantiation : Template β†’ Substitution β†’ Qualifier A qualifier instantiated from a Liquid Haskell template.
read_effect_ty
ReadEffect : Var β†’ Effect β€” Reading from variable.
refinement_inference_ty
RefinementInference : Program β†’ Var β†’ RefinementType Automatically infer strongest safe refinement types.
refinement_type_ty
RefinementType : Type β†’ Pred β†’ Type β€” {x : T | P(x)}.
region_annotation_ty
RegionAnnotation : Expr β†’ Region β€” Maps an expression to its allocation region.
region_inference_ty
RegionInference : Program β†’ RegionAnnotation Infer allocation regions to enable stack allocation of non-escaping values.
region_subtyping_ty
RegionSubtyping : Region β†’ Region β†’ Prop β€” Lifetime/region containment.
region_ty
Region : Type β€” A memory region (stack frame, heap generation, etc.).
resource_type_ty
ResourceType : Type β€” A linear/affine resource type.
resource_usage_analysis_ty
ResourceUsageAnalysis : Program β†’ Var β†’ UsageAnnotation Infers usage count (0, 1, Ο‰) for each variable.
sanitizer_ty
Sanitizer : Type β€” A function that removes taint (e.g., HTML-escape).
secrecy_lattice_ty
SecrecyLattice : SecurityLabel β†’ SecurityLabel β†’ Prop β€” Label ordering βŠ‘.
security_label_ty
SecurityLabel : Type β€” A security lattice element (e.g. Low, High, Secret).
sep_conj_ty
SepConj : SepPred β†’ SepPred β†’ SepPred β€” Separating conjunction P * Q.
sep_imp_ty
SepImp : SepPred β†’ SepPred β†’ SepPred β€” Magic wand P βˆ’βˆ— Q.
sep_logic_heap_ty
SepLogicHeap : Type β€” A heap in separation logic (finite partial map Addr β†’ Val).
set_ty
shape_descriptor_ty
ShapeDescriptor : Type β€” An abstract shape: tree, dag, list, cyclic-list, graph.
shape_join_ty
shape_join : ShapeDescriptor β†’ ShapeDescriptor β†’ ShapeDescriptor
shape_sound_ty
ShapeSound : βˆ€ op s, shape_transfer op s over-approximates concrete shapes
shape_transfer_ty
shape_transfer : HeapOp β†’ ShapeDescriptor β†’ ShapeDescriptor
sharing_pred_ty
SharingPred : HeapGraph β†’ HeapNode β†’ HeapNode β†’ Prop May-sharing: two nodes may alias through some path.
slice_correct_ty
Slice_Correct : βˆ€ prog c, backward_slice preserves criterion semantics
soft_type_check_ty
SoftTypeCheck : Program β†’ SoftType β†’ Bool
soft_type_ty
SoftType : Type β€” A soft type: a type that may be violated at runtime.
steensgaard_almost_linear_ty
Steensgaard_AlmostLinear : Steensgaard is nearly O(n) via union-find
steensgaard_analysis_ty
SteensgaardAnalysis : Program β†’ (Var β†’ Var) β€” Steensgaard unification-based analysis. Returns equivalence classes (union-find representative).
steensgaard_sub_andersen_ty
Steensgaard_SubAndersen : Steensgaard βŠ‘ Andersen (less precise but O(n Ξ±(n)))
string_ty
subtyping_refinement_ty
SubtypingRefinement : RefinementType β†’ RefinementType β†’ Prop {v : B | P} <: {v : B | Q} iff P ⊒ Q.
taint_label_ty
TaintLabel : Var β†’ Bool β€” Is a variable tainted?
taint_no_false_neg_ty
Taint_NoFalseNegatives : all real taint violations are reported
taint_propagation_ty
TaintPropagation : Program β†’ TaintLabel β†’ TaintLabel Propagate taint through the program.
taint_sink_ty
TaintSink : Type β€” A sink that must not receive tainted data (SQL query, shell cmd).
taint_sound_ty
Taint_Sound : βˆ€ prog, taint_propagation over-approximates actual taint flow
taint_source_ty
TaintSource : Type β€” A source of tainted data (user input, env vars, etc.).
taint_violation_ty
TaintViolation : Program β†’ TaintLabel β†’ Set (Var Γ— TaintSink) β†’ Prop A taint violation: tainted variable reaches a sink without sanitization.
thread_ty
Thread : Type β€” An abstract thread identifier.
three_valued_ty
ThreeValued : Type β€” Three-valued logic {True, False, Maybe} for must/may.
tsan_sound_ty
TSan_Sound : ThreadSanitizer reports all races
type0
type_based_alias_ty
TypeBasedAlias : Type β†’ Type β†’ Bool β€” TBAA: types determine alias potential.
typestate_check_ty
TypestateCheck : Program β†’ TypestateProtocol β†’ Prop Program respects the resource usage protocol.
typestate_protocol_ty
TypestateProtocol : Type β€” A resource usage protocol (e.g. Opened/Closed file).
typestate_sound_ty
TypestateSound : typestate analysis is a sound approximation of runtime states
typestate_transition_ty
TypestateTransition : Typestate β†’ Op β†’ Typestate β†’ Prop Specifies valid state transitions under operations.
typestate_ty
Typestate : Type β€” A typestate: a type annotated with a protocol state.
unknown_type_ty
UnknownType : GradualType β€” The dynamic unknown type ?.
usage_annotation_ty
UsageAnnotation : Type β€” Usage count: 0, 1, or Ο‰ (unrestricted).
usage_count_sound_ty
UsageCount_Sound : usage analysis is a sound over-approximation of actual usage
value_range_analysis_ty
ValueRangeAnalysis : Program β†’ Var β†’ IntervalDomain Compute abstract value ranges for all variables.
vra_sound_ty
VRA_Sound : βˆ€ prog, value_range_analysis over-approximates concrete values
widening_terminates_ty
Widening_Terminates : widening guarantees termination of iteration
widening_ty
Widening : AbsDom β†’ AbsDom β†’ AbsDom β€” Widening operator β–½.
write_effect_ty
WriteEffect : Var β†’ Effect β€” Writing to variable.
zero_cfa_ty
ZeroCFA : Program β†’ CallSite β†’ Set AbstractClosure 0-CFA: context-insensitive closure analysis.