asli 0.2.0 (latest) · OCaml Package

ASL interpreter values

module AST = Asl_ast

Values

This union type is for use in an interpreter

type value =

| VBool of bool
| VEnum of LibASL.Asl_utils.AST.ident * int
| VInt of Primops.bigint
| VReal of Primops.real
| VBits of Primops.bitvector
| VMask of Primops.mask
| VString of string
| VExc of LibASL.Asl_utils.AST.l * Primops.exc
| VTuple of value list
| VRecord of value Asl_utils.Bindings.t
| VArray of value Primops.ImmutableArray.t * value
| VRAM of Primops.ram
| 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_integer : LibASL.Asl_utils.AST.l -> value -> Primops.bigint

val to_int : LibASL.Asl_utils.AST.l -> value -> int

val to_bits : LibASL.Asl_utils.AST.l -> value -> Primops.bitvector

val to_mask : LibASL.Asl_utils.AST.l -> value -> Primops.mask

val to_string : LibASL.Asl_utils.AST.l -> value -> string

val to_exc : 
  LibASL.Asl_utils.AST.l ->
  value ->
  LibASL.Asl_utils.AST.l * Primops.exc

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 get_field : 
  LibASL.Asl_utils.AST.l ->
  value ->
  LibASL.Asl_utils.AST.ident ->
  value

val set_field : 
  LibASL.Asl_utils.AST.l ->
  value ->
  LibASL.Asl_utils.AST.ident ->
  value ->
  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

package asli