Safe Haskell	Safe-Inferred
Language	Haskell2010

LibRISCV.Semantics

Description

Functions for interacting with the free monad abstraction used to formally describe the semantics of RISC-V instructions.

Synopsis

buildAST :: forall w v r. (KnownNat w, Member (Operations v) r, Member LogInstructionFetch r, Member (Decoding v) r, Member (ExprEval v) r) => v -> Eff r ()
writeRegister :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => v -> Expr v -> Eff r ()
readRegister :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Expr v -> Eff r v
load :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Size -> Expr v -> Eff r v
store :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Size -> Expr v -> Expr v -> Eff r ()
writePC :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Expr v -> Eff r ()

Documentation

buildAST :: forall w v r. (KnownNat w, Member (Operations v) r, Member LogInstructionFetch r, Member (Decoding v) r, Member (ExprEval v) r) => v -> Eff r () Source #

Obtain the free monad AST for a program loaded into memory, e.g. through the provided ELF Loader implementation. The function takes one argument which corresponds to an address in memory at which program execution will start. An instruction word will be loaded from this address, decoded, and executed.

writeRegister :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => v -> Expr v -> Eff r () Source #

Write to a register in the register file. The function takes a register index and a value which should be written to the register (represented as an Expr). This function is primarly useful to initialize special registers, e.g. setting the stack pointer to a meaningful value at the very beginning of the free monad AST.

readRegister :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Expr v -> Eff r v Source #

Obtain the current value for a register in the register file. The functions takes a register index (encapsulated in an Expr) and returns the value of this register.

load :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Size -> Expr v -> Eff r v Source #

Load a fixed-size value from memory. The function takes two arguments: The Size of the value to load and the start address of the value in memory (represented as an Expr).

store :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Size -> Expr v -> Expr v -> Eff r () Source #

Store a fixed-size value in memory. The arguments are: The Size of the value, the start address where the value should be stored, and the value itself. The latter two are encapuslated in the Expr abstraction.

writePC :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Expr v -> Eff r () Source #

Change the current value of the Program Counter (PC). The new value is the only function argument and is represented as an Expr.