Module LibASL.EvalSource

ASL evaluator

Sourcemodule AST = Asl_ast
Sourcemodule TC = Tcheck
Sourceval trace_write : bool ref

Debugging output on every variable write

Sourceval trace_funcall : bool ref

Debugging output on every function call

Sourceval trace_primop : bool ref

Debugging output on every primitive function or function call

Sourceval trace_instruction : bool ref

Debugging output on every instruction execution

Sourceval 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

Sourcemodule ImpDefs : sig ... end

Scopes

Sourcetype scope = {
  1. mutable bs : Value.value Asl_utils.Bindings.t;
}

Basically just a mutable binding

Sourceval empty_scope : unit -> scope
Sourceval mem_scope : AST.ident -> scope -> bool
Sourceval get_scope : AST.ident -> scope -> Value.value
Sourceval get_scope_opt : AST.ident -> scope -> Value.value option
Sourceval set_scope : AST.ident -> Value.value -> scope -> unit

Mutable bindings

Sourcemodule Env : sig ... end

Environment representing both global and local state of the system

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

Evaluation functions

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

Evaluate bitslice of instruction opcode

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

Evaluate instruction decode pattern match

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

Evaluate list of expressions

Sourceval 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

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

Evaluate UNKNOWN at given type

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

Evaluate pattern match

Evaluate bitslice bounds

Evaluate expression

Sourceval 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)

Sourceval 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.

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

Evaluate list of statements

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

Evaluate statement

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

Evaluate call to function or procedure

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

Evaluate call to function

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

Evaluate call to procedure

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

Evaluate instruction decode case

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

Evaluate instruction decode case alternative

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

Evaluate instruction encoding

Creating environment from global declarations

Sourceval eval_uninitialized : AST.l -> Env.t -> LibASL.Value.AST.ty -> Value.value
Sourceval build_evaluation_environment : LibASL.Value.AST.declaration list -> Env.t

Construct environment from global declarations