package asli

  1. Overview
  2. Docs

ASL interpreter values

module AST = Asl_ast

Values

This union type is for use in an interpreter

type value =
  1. | VBool of bool
  2. | VEnum of LibASL.Asl_utils.AST.ident * int
  3. | VInt of Primops.bigint
  4. | VReal of Primops.real
  5. | VBits of Primops.bitvector
  6. | VMask of Primops.mask
  7. | VString of string
  8. | VExc of LibASL.Asl_utils.AST.l * Primops.exc
  9. | VTuple of value list
  10. | VRecord of value Asl_utils.Bindings.t
  11. | VArray of value Primops.ImmutableArray.t * value
  12. | VRAM of Primops.ram
  13. | VUninitialized

Exceptions thrown by interpreter

exception Return of value option
exception EvalError of LibASL.Asl_utils.AST.l * string
exception Throw of LibASL.Asl_utils.AST.l * Primops.exc

Printer for values

val pp_value : value -> string

Functions on values

val from_bool : bool -> value
val to_bool : LibASL.Asl_utils.AST.l -> value -> bool
val to_int : LibASL.Asl_utils.AST.l -> value -> int
val to_string : LibASL.Asl_utils.AST.l -> value -> string
val to_tuple : value list -> value
val of_tuple : LibASL.Asl_utils.AST.l -> value -> value list
val mkrecord : (LibASL.Asl_utils.AST.ident * value) list -> value
val empty_array : value -> value
val get_array : LibASL.Asl_utils.AST.l -> value -> value -> value
val set_array : LibASL.Asl_utils.AST.l -> value -> value -> value -> value
val drop_chars : string -> char -> string

Delete all characters matching 'c' from string 'x'

val from_intLit : LibASL.Asl_utils.AST.intLit -> value
val from_hexLit : LibASL.Asl_utils.AST.hexLit -> value
val from_realLit : LibASL.Asl_utils.AST.realLit -> value
val from_bitsLit : LibASL.Asl_utils.AST.bitsLit -> value
val from_maskLit : LibASL.Asl_utils.AST.maskLit -> value
val from_stringLit : string -> value

Primop dispatch on values

Returns None iff function does not exist or arguments have wrong type

val eval_prim : string -> value list -> value list -> value option

Utility functions on Values

val extract_bits : LibASL.Asl_utils.AST.l -> value -> value -> value -> value
val extract_bits' : LibASL.Asl_utils.AST.l -> value -> int -> int -> value
val extract_bits'' : LibASL.Asl_utils.AST.l -> value -> value -> value -> value
val insert_bits : LibASL.Asl_utils.AST.l -> value -> value -> value -> value -> value
val insert_bits' : LibASL.Asl_utils.AST.l -> value -> int -> int -> value -> value
val eval_eq : LibASL.Asl_utils.AST.l -> value -> value -> bool
val eval_leq : LibASL.Asl_utils.AST.l -> value -> value -> bool
val eval_eq_int : LibASL.Asl_utils.AST.l -> value -> value -> bool
val eval_eq_bits : LibASL.Asl_utils.AST.l -> value -> value -> bool
val eval_inmask : LibASL.Asl_utils.AST.l -> value -> value -> bool
val eval_add_int : LibASL.Asl_utils.AST.l -> value -> value -> value
val eval_sub_int : LibASL.Asl_utils.AST.l -> value -> value -> value
val eval_concat : LibASL.Asl_utils.AST.l -> value list -> value

Unknown handling

We might want to change this in the future to model the expected non-determinism in the spec. And we might want to augment this with some form of support for uninitialized values (which would ideally trigger an error).

val eval_unknown_bits : Primops.bigint -> value
val eval_unknown_ram : Primops.bigint -> value
val eval_unknown_integer : unit -> value
val eval_unknown_real : unit -> value
val eval_unknown_string : unit -> value
OCaml

Innovation. Community. Security.