Documentation ¶
Index ¶
- Constants
- Variables
- func SetLogger(l *log.Logger)
- type AluOp
- type Assignment
- type Branch
- type Checkpoint
- type EcallFn
- type ElfLoader
- type EmuMode
- type Engine
- type ExitStatus
- type FdTable
- type IHexLoader
- type ImmType
- type Loader
- type Machine
- func (m *Machine) AddCond(cond smt.Bool, checksat bool, s *smt.Solver)
- func (m *Machine) Checkpoint(cond smt.Bool) *Checkpoint
- func (m *Machine) Exec(s *smt.Solver) (isz int32)
- func (m *Machine) Reg(reg uint32) smt.Int32
- func (m *Machine) RegConc(reg uint32) (int32, bool)
- func (m *Machine) RegConcretize(reg uint32, s *smt.Solver) (int32, bool)
- func (m *Machine) SymExit(s *smt.Solver)
- func (m *Machine) SymFail(s *smt.Solver)
- func (m *Machine) SymMarkArray(s *smt.Solver)
- func (m *Machine) SymMarkBytes(s *smt.Solver)
- func (m *Machine) SymPrint(s *smt.Solver)
- func (m *Machine) SymQuietExit(s *smt.Solver)
- func (m *Machine) SysBrk(s *smt.Solver)
- func (m *Machine) SysClose(s *smt.Solver)
- func (m *Machine) SysExit(s *smt.Solver)
- func (m *Machine) SysFstat(s *smt.Solver)
- func (m *Machine) SysLseek(s *smt.Solver)
- func (m *Machine) SysOpen(s *smt.Solver)
- func (m *Machine) SysRead(s *smt.Solver)
- func (m *Machine) SysWrite(s *smt.Solver)
- func (m *Machine) TestCase(s *smt.Solver) (TestCase, bool)
- func (m *Machine) WriteReg(reg uint32, val smt.Int32)
- type Memory
- func (m *Memory) Copy() *Memory
- func (m *Memory) MakeSymAddrRegion(base, length uint32, s *smt.Solver)
- func (m *Memory) Read16(addr smt.Int32, s *smt.Solver) (smt.Int32, bool)
- func (m *Memory) Read16u(addr smt.Int32, s *smt.Solver) (smt.Int32, bool)
- func (m *Memory) Read8(addr smt.Int32, s *smt.Solver) (smt.Int32, bool)
- func (m *Memory) Read8u(addr smt.Int32, s *smt.Solver) (smt.Int32, bool)
- func (m *Memory) ReadBytes(addr uint32, data []byte, s *smt.Solver) bool
- func (m *Memory) ReadWord(addr smt.Int32, s *smt.Solver) (smt.Int32, bool)
- func (m *Memory) Write16(addr, val smt.Int32, s *smt.Solver) bool
- func (m *Memory) Write8(addr, val smt.Int32, s *smt.Solver) bool
- func (m *Memory) WriteBytes(addr uint32, data []byte, s *smt.Solver) bool
- func (m *Memory) WriteWord(addr, val smt.Int32, s *smt.Solver) bool
- type RawLoader
- type Segment
- type Stats
- type Status
- type SymVal
- type SysState
- type TestCase
Constants ¶
View Source
const ( AluAdd = 0b0000000000 AluSub = 0b0100000000 AluSlt = 0b0000000010 AluSltu = 0b0000000011 AluXor = 0b0000000100 AluSll = 0b0000000001 AluSrl = 0b0000000101 AluSra = 0b0100000101 AluOr = 0b0000000110 AluAnd = 0b0000000111 AluMul = 0b0000001000 AluMulH = 0b0000001001 AluMulHSU = 0b0000001010 AluMulHU = 0b0000001011 AluDiv = 0b0000001100 AluDivU = 0b0000001101 AluRem = 0b0000001110 AluRemU = 0b0000001111 )
View Source
const ( ExitNone = iota ExitNormal ExitQuiet ExitFail ExitMem ExitUnsat )
View Source
const ( OpRarith = 0b0110011 OpIarith = 0b0010011 OpBranch = 0b1100011 OpLui = 0b0110111 OpAuipc = 0b0010111 OpJal = 0b1101111 OpJalr = 0b1100111 OpLoad = 0b0000011 OpStore = 0b0100011 OpFence = 0b0001111 OpSys = 0b1110011 OpAtomic = 0b0101111 )
View Source
const ( ExtByte = 0b000 ExtHalf = 0b001 ExtWord = 0b010 ExtByteU = 0b100 ExtHalfU = 0b101 )
View Source
const ( InsnEcall = 0x00000073 InsnEbreak = 0x00100073 InsnNop = 0x00000013 )
View Source
const ( Rzero = iota Rra Rsp Rgp Rtp Rt0 Rt1 Rt2 Rs0 Rs1 Ra0 Ra1 Ra2 Ra3 Ra4 Ra5 Ra6 Ra7 Rs2 Rs3 Rs4 Rs5 Rs6 Rs7 Rs8 Rs9 Rs10 Rs11 Rt3 Rt4 Rt5 Rt6 )
Variables ¶
View Source
var RegNames = map[int]string{
0: "zero",
1: "ra",
2: "sp",
3: "gp",
4: "tp",
5: "t0",
6: "t1",
7: "t2",
8: "s0",
9: "s1",
10: "a0",
11: "a1",
12: "a2",
13: "a3",
14: "a4",
15: "a5",
16: "a6",
17: "a7",
18: "s2",
19: "s3",
20: "s4",
21: "s5",
22: "s6",
23: "s7",
24: "s8",
25: "s9",
26: "s10",
27: "s11",
28: "t3",
29: "t4",
30: "t5",
31: "t6",
}
Functions ¶
Types ¶
type Assignment ¶
type Checkpoint ¶
type Checkpoint struct {
// contains filtered or unexported fields
}
type Engine ¶
type Engine struct { Stats Stats // contains filtered or unexported fields }
func (*Engine) NumTestCases ¶
type ExitStatus ¶
type ExitStatus byte
func (ExitStatus) String ¶
func (e ExitStatus) String() string
type FdTable ¶
type FdTable struct {
// contains filtered or unexported fields
}
func NewFdTable ¶
func NewFdTable() FdTable
type IHexLoader ¶
type IHexLoader struct {
Entry uint32
}
type Machine ¶
type Machine struct { Status Status // contains filtered or unexported fields }
func NewMachine ¶
func (*Machine) Checkpoint ¶
func (m *Machine) Checkpoint(cond smt.Bool) *Checkpoint
func (*Machine) RegConcretize ¶
func (*Machine) SymMarkArray ¶
func (*Machine) SymMarkBytes ¶
func (*Machine) SymQuietExit ¶
type Memory ¶
type Memory struct {
// contains filtered or unexported fields
}
func (*Memory) MakeSymAddrRegion ¶
MakeSymAddrRegion marks the given region as a region of memory that can be symbolically addressed.
func (*Memory) Read16u ¶
Read16u reads the 16-bit unsigned value at addr. Returns false if not found.
func (*Memory) Write16 ¶
Write16 writes a 16-bit value (truncated) at addr. Returns false if the access is out of bounds.
func (*Memory) WriteBytes ¶
type SysState ¶
type SysState struct {
// contains filtered or unexported fields
}
func NewSysState ¶
Source Files ¶
Directories ¶
Path | Synopsis |
---|---|
cmd
|
|
Package hashmap provides an implementation of a hashmap.
|
Package hashmap provides an implementation of a hashmap. |
pkg
|
|
smt/z3
Package z3 checks the satisfiability of logical formulas.
|
Package z3 checks the satisfiability of logical formulas. |
smt/z3/z3log
Package z3log exposes Z3's interaction log.
|
Package z3log exposes Z3's interaction log. |
Package rvc decompresses rv32c instructions
|
Package rvc decompresses rv32c instructions |
Click to show internal directories.
Click to hide internal directories.