package asli

  1. Overview
  2. Docs

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

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

OCaml

Innovation. Community. Security.