Trait CodeGenerator

pub trait CodeGenerator {
    type T;

    // Required methods
    fn leaf_const(&mut self, value: i128) -> Self::T;
    fn leaf_arg(&mut self, arg_index: usize) -> Term<Self::T>;
    fn unknown_op_any(&mut self, name: &str, args: &[Self::T]) -> Self::T;

    // Provided methods
    fn simplify(&mut self, item: Self::T) -> Self::T { ... }
    fn unknown_op1(&mut self, name: &str, item: Self::T) -> Self::T { ... }
    fn unknown_op2(&mut self, name: &str, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn unknown_op3(
        &mut self,
        name: &str,
        arg0: Self::T,
        arg1: Self::T,
        arg2: Self::T,
    ) -> Self::T { ... }
    fn not(&mut self, item: Self::T) -> Self::T { ... }
    fn crop(&mut self, num_bits: u8, item: Self::T) -> Self::T { ... }
    fn sign_extend(&mut self, num_bits: u8, item: Self::T) -> Self::T { ... }
    fn select(&mut self, num_skip: u8, num_take: u8, item: Self::T) -> Self::T { ... }
    fn parity(&mut self, item: Self::T) -> Self::T { ... }
    fn is_zero(&mut self, item: Self::T) -> Self::T { ... }
    fn byte_mask(&mut self, item: Self::T) -> Self::T { ... }
    fn bit_mask(&mut self, item: Self::T) -> Self::T { ... }
    fn trailing_zeros(&mut self, item: Self::T) -> Self::T { ... }
    fn leading_zeros(&mut self, item: Self::T) -> Self::T { ... }
    fn popcount(&mut self, item: Self::T) -> Self::T { ... }
    fn swap_bytes(&mut self, num_bits: u8, item: Self::T) -> Self::T { ... }
    fn add(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn sub(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn mul(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn carryless_mul(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn div(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn div_unsigned(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn rem(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn rem_unsigned(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn shl(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn shr(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn and(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn or(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn xor(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn cmp_lt(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn rol(&mut self, num_bits: u8, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn deposit_bits(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn extract_bits(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T { ... }
    fn if_zero(
        &mut self,
        condition: Self::T,
        if_zero: Self::T,
        if_nonzero: Self::T,
    ) -> Self::T { ... }
}

A code generator that can generate code for computations.

Required Associated Types

type T

An expression in the generated code.

Required Methods

fn leaf_const(&mut self, value: i128) -> Self::T

Create a constant value.

fn leaf_arg(&mut self, arg_index: usize) -> Term<Self::T>

Create a value that loads the argument.

fn unknown_op_any(&mut self, name: &str, args: &[Self::T]) -> Self::T

Generate an error for an unknown operation.

Provided Methods

fn simplify(&mut self, item: Self::T) -> Self::T

Simplify the expression, if possible.

fn unknown_op1(&mut self, name: &str, item: Self::T) -> Self::T

Generate an error for a 1-argument unknown operation.

fn unknown_op2(&mut self, name: &str, lhs: Self::T, rhs: Self::T) -> Self::T

Generate an error for a 2-argument unknown operation.

fn unknown_op3( &mut self, name: &str, arg0: Self::T, arg1: Self::T, arg2: Self::T, ) -> Self::T

Generate an error for a 3-argument unknown operation.

fn not(&mut self, item: Self::T) -> Self::T

Negate the expression.

fn crop(&mut self, num_bits: u8, item: Self::T) -> Self::T

Crop the expression to the lowest num_bits bits.

fn sign_extend(&mut self, num_bits: u8, item: Self::T) -> Self::T

Crop the expression to the lowest num_bits bits, then sign-extend it.

fn select(&mut self, num_skip: u8, num_take: u8, item: Self::T) -> Self::T

Select num_take bits starting at bit index num_skip from item.

fn parity(&mut self, item: Self::T) -> Self::T

Crop the expression to the lowest 8 bits, then compute the parity.

fn is_zero(&mut self, item: Self::T) -> Self::T

Return ‘1’ if the expression is zero, otherwise return ‘0’.

fn byte_mask(&mut self, item: Self::T) -> Self::T

Return the byte mask for the expression.

fn bit_mask(&mut self, item: Self::T) -> Self::T

Return a bit mask for the given number of bits.

fn trailing_zeros(&mut self, item: Self::T) -> Self::T

Count the number of trailing zeros.

fn leading_zeros(&mut self, item: Self::T) -> Self::T

Count the number of leading zeros.

fn popcount(&mut self, item: Self::T) -> Self::T

Count the number of ones.

fn swap_bytes(&mut self, num_bits: u8, item: Self::T) -> Self::T

Reverse the order of the lowest ceil(num_bits / 8) bytes.

fn add(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Add two values.

fn sub(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Subtract rhs from lhs.

fn mul(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Multiply two values.

fn carryless_mul(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Perform carryless multiplication.

fn div(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Perform signed division.

fn div_unsigned(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Perform unsigned division.

fn rem(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Compute the signed remainder.

fn rem_unsigned(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Compute the unsigned remainder.

fn shl(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Shift lhs left by rhs positions.

fn shr(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Shift lhs right by rhs positions.

fn and(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Compute the bitwise AND.

fn or(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Compute the bitwise OR.

fn xor(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Compute the bitwise XOR.

fn cmp_lt(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Return ‘1’ if lhs is less than rhs, return ‘1’ otherwise.

fn rol(&mut self, num_bits: u8, lhs: Self::T, rhs: Self::T) -> Self::T

Crop lhs to num_bits, then rotate those bits rhs positions.

fn deposit_bits(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Perform the PDEP operation.

fn extract_bits(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Perform the PEXT operation

fn if_zero( &mut self, condition: Self::T, if_zero: Self::T, if_nonzero: Self::T, ) -> Self::T

If condition is zero, return if_zero. Otherwise, return if_nonzero.

Implementors

impl CodeGenerator for SExprCodeGen

type T = SExpr

impl<'ctx, S: SmtSolver<'ctx>> CodeGenerator for Z3CodeGen<'_, 'ctx, S>

type T = Z3Expr<'ctx, S>