Classes
class	ActionDarkSolver

class	ActionMochaSolver

class	ActionMoveSolver

class	ActionSolverBase
	ActionSolverBase contains basic methods and states for all solvers. More...

struct	Assign
	Assign is a set instruction that move operand src bits to dst. More...

class	BitmaskedSet

class	ByteRotateMerge

class	ContainerSet

struct	ContainerSpec
	ContainerSpec container specification. More...

class	DepositField

struct	Error
	Error type for all solver. More...

class	Instruction

struct	Operand
	Operand represents either a source or a destination of an instruction. More...

struct	Result
	Result contains either an error or all instructions for an action. More...

Typedefs
using	ContainerID = cstring

using	RotateClassifiedAssigns = std::map<int, std::vector<Assign>>
	right-rotate-offset-indexed assignments.

Enumerations
enum class	ErrorCode { unsat = 1 , invalid_input = 2 , too_many_container_sources = 3 , too_many_unaligned_sources = 4 , invalid_for_deposit_field = 5 , smt_sovler_unknown = 6 , deposit_src2_must_be_dest = 7 , non_rot_aligned_and_non_byte_shiftable = 8 , invalid_whole_container_write = 9 , dark_container_ad_or_const_source = 10 }

Functions
Operand	make_ad_or_const_operand ()
	Constructor helper functions for operand.

Operand	make_container_operand (ContainerID c, le_bitrange r)

std::ostream &	operator<< (std::ostream &s, const Assign &c)

std::ostream &	operator<< (std::ostream &s, const Operand &c)

std::ostream &	operator<< (std::ostream &s, const std::vector< Assign > &c)

Detailed Description

Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.

SPDX-License-Identifier: Apache-2.0

Class Documentation

◆ solver::Assign

struct solver::Assign

Assign is a set instruction that move operand src bits to dst.

Class Members
Operand	dst
Operand	src

◆ solver::ContainerSpec

struct solver::ContainerSpec

ContainerSpec container specification.

Class Members
bitvec	live	bits that will have live fieldslices allocated, after action.
int	size

Typedef Documentation

◆ ContainerID

using solver::ContainerID = cstring

ContainerID is a cstring that uniquely represents a container. Empty string is reserved to represent const or action data.

Classes

Typedefs