Information about the prime finite field used for the interval analysis. More...

#include <Field.h>

Public Member Functions
	Field ()=delete
	Field (const Field &)=default
	Field (Field &&) noexcept=default
Field &	operator= (const Field &)=default
llvm::DynamicAPInt	prime () const
	For the prime field p, returns p.
llvm::DynamicAPInt	half () const
	Returns p / 2.
llvm::DynamicAPInt	felt (int i) const
	Returns i as a signed field element.
llvm::DynamicAPInt	zero () const
	Returns 0 at the bitwidth of the field.
llvm::DynamicAPInt	one () const
	Returns 1 at the bitwidth of the field.
llvm::DynamicAPInt	maxVal () const
	Returns p - 1, which is the max value possible in a prime field described by p.
llvm::DynamicAPInt	inv (const llvm::DynamicAPInt &i) const
	Returns the multiplicative inverse of i in prime field p.
llvm::DynamicAPInt	inv (const llvm::APInt &i) const
llvm::DynamicAPInt	reduce (const llvm::DynamicAPInt &i) const
	Returns i mod p and reduces the result into the appropriate bitwidth.
llvm::DynamicAPInt	reduce (int i) const
llvm::DynamicAPInt	reduce (const llvm::APInt &i) const
llvm::DynamicAPInt	toSigned (const llvm::DynamicAPInt &i) const
	Converts a canonical field element to its signed integer representation: toSigned(f) = f if f < field.half() toSigned(f) = f - p if f >= field.half() (field.half() == ceil(p/2) == floor(p/2) + 1 for odd prime p)
unsigned	bitWidth () const
llvm::StringRef	name () const
llvm::SMTExprRef	createSymbol (const llvm::SMTSolverRef &solver, const char *name) const
	Create a SMT solver symbol with the current field's bitwidth.

Static Public Member Functions
static void	addField (llvm::StringRef fieldName, const llvm::APInt &prime, EmitErrorFn errFn)
	Add a new field to the set of available prime fields.
static void	addField (llvm::StringRef fieldName, llvm::StringRef primeStr, EmitErrorFn errFn)
static llvm::FailureOr< std::reference_wrapper< const Field > >	tryGetField (llvm::StringRef fieldName)
	Get a Field from a given field name string, or failure if the field is not defined.
static llvm::LogicalResult	verifyFieldDefined (llvm::StringRef fieldName, EmitErrorFn errFn)
	Search for a field with the given name, reporting an error if the field is not found.
static const Field &	getField (llvm::StringRef fieldName, EmitErrorFn errFn)
	Get a Field from a given field name string.
static const Field &	getField (llvm::StringRef fieldName)

Friends
bool	operator== (const Field &lhs, const Field &rhs)
bool	operator< (const Field &lhs, const Field &rhs)

Detailed Description

Information about the prime finite field used for the interval analysis.

Note: See implementation of initKnownFields for supported primes.; We use DynamicAPInt to support arithmetic that may require increasing or signed arithmetic (e.g., multiplying field elements before applying the modulus).

Definition at line 35 of file Field.h.

Constructor & Destructor Documentation

◆ Field() [1/3]

llzk::Field::Field ( )

delete

◆ Field() [2/3]

llzk::Field::Field ( const Field & )

default

◆ Field() [3/3]

llzk::Field::Field ( Field && )

defaultnoexcept

Member Function Documentation

◆ addField() [1/2]

void llzk::Field::addField	(	llvm::StringRef	fieldName,
		const llvm::APInt &	prime,
		EmitErrorFn	errFn )

inlinestatic

Add a new field to the set of available prime fields.

Reports an error if the field is invalid or conflicts with an existing definition.

Definition at line 40 of file Field.h.

◆ addField() [2/2]

void llzk::Field::addField	(	llvm::StringRef	fieldName,
		llvm::StringRef	primeStr,
		EmitErrorFn	errFn )

inlinestatic

Definition at line 44 of file Field.h.

◆ bitWidth()

unsigned llzk::Field::bitWidth ( ) const

inline

Definition at line 106 of file Field.h.

◆ createSymbol()

llvm::SMTExprRef llzk::Field::createSymbol	(	const llvm::SMTSolverRef &	solver,
		const char *	name ) const

inline

Create a SMT solver symbol with the current field's bitwidth.

Definition at line 111 of file Field.h.

◆ felt()

llvm::DynamicAPInt llzk::Field::felt ( int i ) const

inline

Returns i as a signed field element.

Definition at line 77 of file Field.h.

◆ getField() [1/2]

const Field & llzk::Field::getField ( llvm::StringRef fieldName )

inlinestatic

Definition at line 61 of file Field.h.

◆ getField() [2/2]

const Field & llzk::Field::getField	(	llvm::StringRef	fieldName,
		EmitErrorFn	errFn )

static

Get a Field from a given field name string.

Throws a fatal error if the field is unsupported.

Parameters

fieldName The name of the field.

◆ half()

llvm::DynamicAPInt llzk::Field::half ( ) const

inline

Returns p / 2.

Definition at line 74 of file Field.h.

◆ inv() [1/2]

llvm::DynamicAPInt llzk::Field::inv ( const llvm::APInt & i ) const

◆ inv() [2/2]

llvm::DynamicAPInt llzk::Field::inv ( const llvm::DynamicAPInt & i ) const

Returns the multiplicative inverse of i in prime field p.

◆ maxVal()

llvm::DynamicAPInt llzk::Field::maxVal ( ) const

inline

Returns p - 1, which is the max value possible in a prime field described by p.

Definition at line 86 of file Field.h.

◆ name()

llvm::StringRef llzk::Field::name ( ) const

inline

Definition at line 108 of file Field.h.

◆ one()

llvm::DynamicAPInt llzk::Field::one ( ) const

inline

Returns 1 at the bitwidth of the field.

Definition at line 83 of file Field.h.

◆ operator=()

Field & llzk::Field::operator= ( const Field & )

default

◆ prime()

llvm::DynamicAPInt llzk::Field::prime ( ) const

inline

For the prime field p, returns p.

Definition at line 71 of file Field.h.

◆ reduce() [1/3]

llvm::DynamicAPInt llzk::Field::reduce ( const llvm::APInt & i ) const

◆ reduce() [2/3]

llvm::DynamicAPInt llzk::Field::reduce ( const llvm::DynamicAPInt & i ) const

Returns i mod p and reduces the result into the appropriate bitwidth.

Field elements are returned as signed integers so that negation functions as expected (i.e., reducing -1 will yield p-1).

◆ reduce() [3/3]

llvm::DynamicAPInt llzk::Field::reduce ( int i ) const

inline

Definition at line 97 of file Field.h.

◆ toSigned()

DynamicAPInt llzk::Field::toSigned ( const llvm::DynamicAPInt & i ) const

Converts a canonical field element to its signed integer representation: toSigned(f) = f if f < field.half() toSigned(f) = f - p if f >= field.half() (field.half() == ceil(p/2) == floor(p/2) + 1 for odd prime p)

Definition at line 131 of file Field.cpp.

◆ tryGetField()

FailureOr< std::reference_wrapper< const Field > > llzk::Field::tryGetField ( llvm::StringRef fieldName )

static

Get a Field from a given field name string, or failure if the field is not defined.

Parameters

fieldName The name of the field.

Definition at line 50 of file Field.cpp.

◆ verifyFieldDefined()

LogicalResult llzk::Field::verifyFieldDefined	(	llvm::StringRef	fieldName,
		EmitErrorFn	errFn )

static

Search for a field with the given name, reporting an error if the field is not found.

Definition at line 60 of file Field.cpp.

◆ zero()

llvm::DynamicAPInt llzk::Field::zero ( ) const

inline

Returns 0 at the bitwidth of the field.

Definition at line 80 of file Field.h.

◆ operator<

bool operator<	(	const Field &	lhs,
		const Field &	rhs )

friend

Definition at line 119 of file Field.h.

◆ operator==

bool operator==	(	const Field &	lhs,
		const Field &	rhs )

friend

Definition at line 115 of file Field.h.

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

include/llzk/Util/Field.h
lib/Util/Field.cpp

Public Member Functions

Static Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Field() [1/3]

◆ Field() [2/3]

◆ Field() [3/3]

Member Function Documentation

◆ addField() [1/2]

◆ addField() [2/2]

◆ bitWidth()

◆ createSymbol()

◆ felt()

◆ getField() [1/2]

◆ getField() [2/2]

◆ half()

◆ inv() [1/2]

◆ inv() [2/2]

◆ maxVal()

◆ name()

◆ one()

◆ operator=()

◆ prime()

◆ reduce() [1/3]

◆ reduce() [2/3]

◆ reduce() [3/3]

◆ toSigned()

◆ tryGetField()

◆ verifyFieldDefined()

◆ zero()

Friends And Related Symbol Documentation

◆ operator<

◆ operator==