LLZK 0.1.0
Veridise's ZK Language IR
Loading...
Searching...
No Matches
llzk::Interval Class Reference

Intervals over a finite field. More...

#include <IntervalAnalysis.h>

Classes

struct  Hash
 

Public Types

enum class  Type {
  TypeA = 0 , TypeB , TypeC , TypeF ,
  Empty , Degenerate , Entire
}
 

Public Member Functions

 Interval ()
 To satisfy the dataflow::ScalarLatticeValue requirements, this class must be default initializable.
 
UnreducedInterval toUnreduced () const
 Convert to an UnreducedInterval.
 
UnreducedInterval firstUnreduced () const
 Get the first side of the interval for TypeF intervals, otherwise just get the full interval as an UnreducedInterval (with toUnreduced).
 
UnreducedInterval secondUnreduced () const
 Get the second side of the interval for TypeA, TypeB, and TypeC intervals.
 
Interval join (const Interval &rhs) const
 Union.
 
Interval intersect (const Interval &rhs) const
 Intersect.
 
Interval difference (const Interval &other) const
 Computes and returns this - (this & other) if the operation produces a single interval.
 
Interval operator- () const
 
bool isEmpty () const
 
bool isNotEmpty () const
 
bool isDegenerate () const
 
bool isEntire () const
 
bool isTypeA () const
 
bool isTypeB () const
 
bool isTypeC () const
 
bool isTypeF () const
 
template<Type... Types>
bool is () const
 
bool operator== (const Interval &rhs) const
 
const FieldgetField () const
 
llvm::APSInt width () const
 
llvm::APSInt lhs () const
 
llvm::APSInt rhs () const
 
void print (mlir::raw_ostream &os) const
 

Static Public Member Functions

static std::string_view TypeName (Type t)
 
static Interval Empty (const Field &f)
 
static Interval Degenerate (const Field &f, llvm::APSInt val)
 
static Interval Boolean (const Field &f)
 
static Interval Entire (const Field &f)
 
static Interval TypeA (const Field &f, llvm::APSInt a, llvm::APSInt b)
 
static Interval TypeB (const Field &f, llvm::APSInt a, llvm::APSInt b)
 
static Interval TypeC (const Field &f, llvm::APSInt a, llvm::APSInt b)
 
static Interval TypeF (const Field &f, llvm::APSInt a, llvm::APSInt b)
 
template<std::pair< Type, Type >... Pairs>
static bool areOneOf (const Interval &a, const Interval &b)
 

Static Public Attributes

static constexpr std::array< std::string_view, 7 > TypeNames
 

Friends

Interval operator+ (const Interval &lhs, const Interval &rhs)
 
Interval operator- (const Interval &lhs, const Interval &rhs)
 
Interval operator* (const Interval &lhs, const Interval &rhs)
 
Interval operator% (const Interval &lhs, const Interval &rhs)
 
mlir::FailureOr< Intervaloperator/ (const Interval &lhs, const Interval &rhs)
 Returns failure if a division-by-zero is encountered.
 
mlir::raw_ostream & operator<< (mlir::raw_ostream &os, const Interval &i)
 

Detailed Description

Intervals over a finite field.

Based on the Picus implementation. An interval may be:

  • Empty
  • Entire (meaning any value across the entire field)
  • Degenerate (meaning it contains a single value)
  • Or Type A–F. For these types, refer to the below notes:

A range [a, b] can be split into 2 categories:

  • Internal: a <= b
  • External: a > b – equivalent to [a, p-1] U [0, b]

Internal range can be further split into 3 categories: (A) a, b < p/2. E.g., [10, 12] (B) a, b > p/2. OR: a, b \in {-p/2, 0}. E.g., [p-4, p-2] === [-4, -2] (C) a < p/2, b > p/2. E.g., [p/2 - 5, p/2 + 5]

External range can be further split into 3 categories: (D) a, b < p/2. OR: a \in {-p, -p/2}, b \in {0, p/2}. E.g., [12, 10] === [-p+12, 10] (E) a, b > p/2. OR: a \in {-p/2, 0} , b \in {p/2, p}. E.g., [p-2, p-4] === [-2, p-4] (F) a > p/2, b < p/2. OR: a \in {-p/2, 0} , b \in {0, p/2}. E.g., [p/2 + 5, p/2 - 5] === [-p/2 + 5, p/2 - 5]

<-------------------------------------------------------------> -p -p/2 0 p/2 p [ A ] [ A ] [ B ] [ B ] [ C ] [ C ] F ] [ F ] [ F <------------------------------------------------------------->

D ] [ D ] [ D ] E ] [ E ] [ E

For the sake of simplicity, let's just not care about D and E, which covers at least half of the field, and potentially more.

Now, there are 4 choose 2 possible non-self interactions:

A acts on B:

  • intersection: impossible
  • union: C or F

A acts on C:

  • intersection: A
  • union: C

A acts on F:

  • intersection: A
  • union: F

B acts on C

  • intersection: B
  • union: C

B acts on F:

  • intersection: B
  • union: F

C acts on F:

  • intersection: A, B, C, F

    E.g. [p/2 - 10, p/2 + 10] intersects [-p/2 + 2, p/2 - 2]

    = ((-p/2 - 10, -p/2 + 10) intersects (-p/2 + 2, p/2 - 2)) union (( p/2 - 10, p/2 + 10) intersects (-p/2 + 2, p/2 - 2))

    = (-p/2 + 2, -p/2 + 10) union (p/2 - 10, p/2 - 2)

  • union: don't care for now, we can revisit this later.

Definition at line 290 of file IntervalAnalysis.h.

Member Enumeration Documentation

◆ Type

enum class llzk::Interval::Type
strong
Enumerator
TypeA 
TypeB 
TypeC 
TypeF 
Empty 
Degenerate 
Entire 

Definition at line 292 of file IntervalAnalysis.h.

Constructor & Destructor Documentation

◆ Interval()

llzk::Interval::Interval ( )
inline

To satisfy the dataflow::ScalarLatticeValue requirements, this class must be default initializable.

The default interval is the full range of values.

Definition at line 329 of file IntervalAnalysis.h.

Member Function Documentation

◆ areOneOf()

template<std::pair< Type, Type >... Pairs>
static bool llzk::Interval::areOneOf ( const Interval & a,
const Interval & b )
inlinestatic

Definition at line 343 of file IntervalAnalysis.h.

◆ Boolean()

static Interval llzk::Interval::Boolean ( const Field & f)
inlinestatic

Definition at line 307 of file IntervalAnalysis.h.

◆ Degenerate()

static Interval llzk::Interval::Degenerate ( const Field & f,
llvm::APSInt val )
inlinestatic

Definition at line 303 of file IntervalAnalysis.h.

◆ difference()

Interval llzk::Interval::difference ( const Interval & other) const

Computes and returns this - (this & other) if the operation produces a single interval.

Note that this is an interval difference, not a subtraction operation like the operator- below.

For example, given *this = [1, 10] and other = [5, 11], this function would return [1, 4], as this & other (the intersection) = [5, 10], so [1, 10] - [5, 10] = [1, 4].

For example, given *this = [1, 10] and other = [5, 6], this function should return [1, 4] and [7, 10], but we don't support having multiple disjoint intervals, so this is returned as-is.

Definition at line 345 of file IntervalAnalysis.cpp.

◆ Empty()

static Interval llzk::Interval::Empty ( const Field & f)
inlinestatic

Definition at line 301 of file IntervalAnalysis.h.

◆ Entire()

static Interval llzk::Interval::Entire ( const Field & f)
inlinestatic

Definition at line 309 of file IntervalAnalysis.h.

◆ firstUnreduced()

UnreducedInterval llzk::Interval::firstUnreduced ( ) const

Get the first side of the interval for TypeF intervals, otherwise just get the full interval as an UnreducedInterval (with toUnreduced).

Definition at line 213 of file IntervalAnalysis.cpp.

◆ getField()

const Field & llzk::Interval::getField ( ) const
inline

Definition at line 395 of file IntervalAnalysis.h.

◆ intersect()

Interval llzk::Interval::intersect ( const Interval & rhs) const

Intersect.

Definition at line 281 of file IntervalAnalysis.cpp.

◆ is()

template<Type... Types>
bool llzk::Interval::is ( ) const
inline

Definition at line 389 of file IntervalAnalysis.h.

◆ isDegenerate()

bool llzk::Interval::isDegenerate ( ) const
inline

Definition at line 382 of file IntervalAnalysis.h.

◆ isEmpty()

bool llzk::Interval::isEmpty ( ) const
inline

Definition at line 380 of file IntervalAnalysis.h.

◆ isEntire()

bool llzk::Interval::isEntire ( ) const
inline

Definition at line 383 of file IntervalAnalysis.h.

◆ isNotEmpty()

bool llzk::Interval::isNotEmpty ( ) const
inline

Definition at line 381 of file IntervalAnalysis.h.

◆ isTypeA()

bool llzk::Interval::isTypeA ( ) const
inline

Definition at line 384 of file IntervalAnalysis.h.

◆ isTypeB()

bool llzk::Interval::isTypeB ( ) const
inline

Definition at line 385 of file IntervalAnalysis.h.

◆ isTypeC()

bool llzk::Interval::isTypeC ( ) const
inline

Definition at line 386 of file IntervalAnalysis.h.

◆ isTypeF()

bool llzk::Interval::isTypeF ( ) const
inline

Definition at line 387 of file IntervalAnalysis.h.

◆ join()

Interval llzk::Interval::join ( const Interval & rhs) const

Union.

Definition at line 225 of file IntervalAnalysis.cpp.

◆ lhs()

llvm::APSInt llzk::Interval::lhs ( ) const
inline

Definition at line 399 of file IntervalAnalysis.h.

◆ operator-()

Interval llzk::Interval::operator- ( ) const

Definition at line 408 of file IntervalAnalysis.cpp.

◆ operator==()

bool llzk::Interval::operator== ( const Interval & rhs) const
inline

Definition at line 391 of file IntervalAnalysis.h.

◆ print()

void llzk::Interval::print ( mlir::raw_ostream & os) const

Definition at line 457 of file IntervalAnalysis.cpp.

◆ rhs()

llvm::APSInt llzk::Interval::rhs ( ) const
inline

Definition at line 400 of file IntervalAnalysis.h.

◆ secondUnreduced()

UnreducedInterval llzk::Interval::secondUnreduced ( ) const

Get the second side of the interval for TypeA, TypeB, and TypeC intervals.

Using this function is an error for all other interval types.

Definition at line 220 of file IntervalAnalysis.cpp.

◆ toUnreduced()

UnreducedInterval llzk::Interval::toUnreduced ( ) const

Convert to an UnreducedInterval.

Definition at line 203 of file IntervalAnalysis.cpp.

◆ TypeA()

static Interval llzk::Interval::TypeA ( const Field & f,
llvm::APSInt a,
llvm::APSInt b )
inlinestatic

Definition at line 311 of file IntervalAnalysis.h.

◆ TypeB()

static Interval llzk::Interval::TypeB ( const Field & f,
llvm::APSInt a,
llvm::APSInt b )
inlinestatic

Definition at line 315 of file IntervalAnalysis.h.

◆ TypeC()

static Interval llzk::Interval::TypeC ( const Field & f,
llvm::APSInt a,
llvm::APSInt b )
inlinestatic

Definition at line 319 of file IntervalAnalysis.h.

◆ TypeF()

static Interval llzk::Interval::TypeF ( const Field & f,
llvm::APSInt a,
llvm::APSInt b )
inlinestatic

Definition at line 323 of file IntervalAnalysis.h.

◆ TypeName()

static std::string_view llzk::Interval::TypeName ( Type t)
inlinestatic

Definition at line 297 of file IntervalAnalysis.h.

◆ width()

llvm::APSInt llzk::Interval::width ( ) const
inline

Definition at line 397 of file IntervalAnalysis.h.

Friends And Related Symbol Documentation

◆ operator%

Interval operator% ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 449 of file IntervalAnalysis.cpp.

◆ operator*

Interval operator* ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 417 of file IntervalAnalysis.cpp.

◆ operator+

Interval operator+ ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 410 of file IntervalAnalysis.cpp.

◆ operator-

Interval operator- ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 415 of file IntervalAnalysis.cpp.

◆ operator/

mlir::FailureOr< Interval > operator/ ( const Interval & lhs,
const Interval & rhs )
friend

Returns failure if a division-by-zero is encountered.

Definition at line 437 of file IntervalAnalysis.cpp.

◆ operator<<

mlir::raw_ostream & operator<< ( mlir::raw_ostream & os,
const Interval & i )
friend

Definition at line 412 of file IntervalAnalysis.h.

Member Data Documentation

◆ TypeNames

std::array<std::string_view, 7> llzk::Interval::TypeNames
staticconstexpr
Initial value:
= {"TypeA", "TypeB", "TypeC",
"TypeF", "Empty", "Degenerate",
"Entire"}

Definition at line 293 of file IntervalAnalysis.h.


The documentation for this class was generated from the following files: