reasoner/datalog/datalog_engine library
Classes
- AllocRule
- VarPointsTo(var, heap) :- Assign(var, alloc), Alloc(alloc, heap).
- CallGraphRule
- CallGraph(site, method) :- Call(site, receiver, method, _), VarPointsTo(receiver, _).
- CopyRule
- VarPointsTo(var1, heap) :- Assign(var1, var2), VarPointsTo(var2, heap).
- DatalogEngine
- Datalog engine interface for relational reasoning.
- DatalogRule
- A Datalog rule with stratification support.
- Fact
- A Datalog fact (tuple in a relation).
- ImmutabilityRule
- DeepImmutable(heap) :- Alloc(_, heap), !Mutable(heap).
- InMemoryDatalogEngine
- In-memory Datalog engine for testing and small programs.
- LoadFieldRule
- VarPointsTo(target, targetHeap) :- LoadField(base, field, target), VarPointsTo(base, baseHeap), HeapPointsTo(baseHeap, field, targetHeap).
- MutabilityRule
- Mutable(heap) :- StoreField(base, _, _), VarPointsTo(base, heap).
- PointsToEngineFactory
- Factory to create a fully configured points-to analysis engine.
- ReachabilityRule
- Reachable(to) :- Reachable(from), Flow(from, to).
- SouffleEngine
- Native Soufflé engine integration via FFI.
- StoreFieldRule
- HeapPointsTo(baseHeap, field, targetHeap) :- StoreField(base, field, source), VarPointsTo(base, baseHeap), VarPointsTo(source, targetHeap).
- TaintEngineFactory
- Factory to create a taint tracking analysis engine.
- TaintLoadFieldRule
- TaintedVar(target, source, label) :- LoadField(base, field, target), VarPointsTo(base, baseHeap), TaintedHeap(baseHeap, field, source, label).
- TaintPropagationRule
- TaintedVar(target, source, label) :- Assign(target, from), TaintedVar(from, source, label).
- TaintSourceRule
- TaintedVar(var, source, label) :- TaintSource(var, label).
- TaintStoreFieldRule
- TaintedHeap(baseHeap, field, source, label) :- StoreField(base, field, sourceVar), VarPointsTo(base, baseHeap), TaintedVar(sourceVar, source, label).
- TaintViolationRule
- TaintViolation(sink, source, taintLabel, sinkLabel) :- TaintSink(sink, sinkLabel), TaintedVar(sink, source, taintLabel).
- TransitiveMutabilityRule
- Mutable(heap) :- HeapPointsTo(heap, _, targetHeap), Mutable(targetHeap). (Transitive mutability)