Module `LibASL.Eval`Source

ASL evaluator

Sourcemodule PP = Asl_parser_pp

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 = {

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

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

Evaluation functions

Source

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

Evaluate bitslice of instruction opcode

Source

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

Evaluate instruction decode pattern match

Source

val 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

Source

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

Evaluate pattern match

Source

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

Evaluate bitslice bounds

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

Evaluate expression

Source

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)

Source

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.

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

Source

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

Evaluate call to function or procedure

Source

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

Evaluate call to function

Source

val 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

Source

val 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/asli.libASL/LibASL/Eval/index.html

Module `LibASL.Eval`Source

Lookup table for IMPLEMENTATION_DEFINED values

Scopes

Mutable bindings

Evaluation functions

Creating environment from global declarations

package asli

Install

Dune Dependency

Authors

Maintainers

Sources

doc/asli.libASL/LibASL/Eval/index.html

Module LibASL.EvalSource

Lookup table for IMPLEMENTATION_DEFINED values

Scopes

Mutable bindings

Evaluation functions

Creating environment from global declarations

Module `LibASL.Eval`Source