asli 0.2.0 (latest) · OCaml Package

ASL evaluator

module PP = Asl_parser_pp

module AST = Asl_ast

module TC = Tcheck

val trace_write : bool Stdlib.ref

Debugging output on every variable write

val trace_funcall : bool Stdlib.ref

Debugging output on every function call

val trace_primop : bool Stdlib.ref

Debugging output on every primitive function or function call

val trace_instruction : bool Stdlib.ref

Debugging output on every instruction execution

val override_conflicts : bool

It is an error to have multiple function definitions with conflicting types. * But, for historical reasons, we still allow multiple definitions and later * definitions override earlier definitions.

Lookup table for IMPLEMENTATION_DEFINED values

module ImpDefs : sig ... end

Scopes

type scope = {

mutable bs : Value.value Asl_utils.Bindings.t;

}

Basically just a mutable binding

val empty_scope : unit -> scope

val mem_scope : AST.ident -> scope -> bool

val get_scope : AST.ident -> scope -> Value.value

val get_scope_opt : AST.ident -> scope -> Value.value option

val set_scope : AST.ident -> Value.value -> scope -> unit

Mutable bindings

module Env : sig ... end

Environment representing both global and local state of the system

val isGlobalConst : Env.t -> LibASL.Value.AST.ident -> bool

val removeGlobalConsts : Env.t -> Asl_utils.IdentSet.t -> Asl_utils.IdentSet.t

Evaluation functions

val eval_decode_slice : 
  AST.l ->
  Env.t ->
  AST.decode_slice ->
  Value.value ->
  Value.value

Evaluate bitslice of instruction opcode

val eval_decode_pattern : 
  LibASL.Value.AST.l ->
  AST.decode_pattern ->
  Value.value ->
  bool

Evaluate instruction decode pattern match

val eval_exprs : 
  AST.l ->
  Env.t ->
  LibASL.Value.AST.expr list ->
  Value.value list

Evaluate list of expressions

val mk_uninitialized : AST.l -> Env.t -> LibASL.Value.AST.ty -> Value.value

Create uninitialized value at given type

For any scalar type, this is the value VUninitialized.
For any composite type, all elements are set to uninitialized values

todo: bitvectors are currently set to UNKNOWN because the bitvector representation currently in use cannot track uninitialized bits

val eval_unknown : AST.l -> Env.t -> LibASL.Value.AST.ty -> Value.value

Evaluate UNKNOWN at given type

val eval_pattern : 
  AST.l ->
  Env.t ->
  Value.value ->
  LibASL.Value.AST.pattern ->
  bool

Evaluate pattern match

val eval_slice : 
  AST.l ->
  Env.t ->
  LibASL.Value.AST.slice ->
  Value.value * Value.value

Evaluate bitslice bounds

val eval_expr : AST.l -> Env.t -> LibASL.Value.AST.expr -> Value.value

Evaluate expression

val eval_lexpr : 
  AST.l ->
  Env.t ->
  LibASL.Value.AST.lexpr ->
  Value.value ->
  unit

Evaluate L-expression in write-mode (i.e., this is not a read-modify-write)

val eval_lexpr_modify : 
  AST.l ->
  Env.t ->
  AST.lexpr ->
  (Value.value -> Value.value) ->
  unit

Evaluate L-expression in read-modify-write mode.

1. The old value of the L-expression is read. 2. The function 'modify' is applied to the old value 3. The result is written back to the L-expression.

val eval_stmts : Env.t -> LibASL.Value.AST.stmt list -> unit

Evaluate list of statements

val eval_stmt : Env.t -> LibASL.Value.AST.stmt -> unit

Evaluate statement

val eval_call : 
  AST.l ->
  Env.t ->
  AST.ident ->
  Value.value list ->
  Value.value list ->
  unit

Evaluate call to function or procedure

val eval_funcall : 
  AST.l ->
  Env.t ->
  AST.ident ->
  Value.value list ->
  Value.value list ->
  Value.value

Evaluate call to function

val eval_proccall : 
  AST.l ->
  Env.t ->
  AST.ident ->
  Value.value list ->
  Value.value list ->
  unit

Evaluate call to procedure

val eval_decode_case : AST.l -> Env.t -> AST.decode_case -> Value.value -> unit

Evaluate instruction decode case

val eval_decode_alt : 
  AST.l ->
  Env.t ->
  AST.decode_alt ->
  Value.value list ->
  Value.value ->
  bool

Evaluate instruction decode case alternative

val eval_encoding : Env.t -> AST.encoding -> Value.value -> bool

Evaluate instruction encoding

Creating environment from global declarations

val eval_uninitialized : AST.l -> Env.t -> LibASL.Value.AST.ty -> Value.value

val build_evaluation_environment : LibASL.Value.AST.declaration list -> Env.t

Construct environment from global declarations

package asli

Lookup table for IMPLEMENTATION_DEFINED values

Scopes

Mutable bindings

Evaluation functions

Creating environment from global declarations