Make (soteria-c.Soteria_c_lib.Interp.Make)

Parameters

module State : State_intf.S

Signature

module InterpM : sig ... end

module Stubs : sig ... end

exception Unsupported of string * Cerb_location.t

val type_of : 
  Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.expression ->
  Cerb_frontend.Ctype.ctype

val unwrap_ctype : Ctype.ctype -> Ctype.ctype_

val pointer_inner : Ctype.ctype -> Ctype.ctype option

type state = State.t

val cast_aggregate_to_ptr : Agv.t -> [ `Ptr ] Typed.t Csymex.t

val cast_to_int : 
  [< T.cval ] Typed.t ->
  [> Soteria__Bv_values__Typed.T.sint ] Typed.t Csymex.t

val cast_aggregate_to_int : 
  Agv.t ->
  [> Soteria__Bv_values__Typed.T.sint ] Typed.t Csymex.t

val cast_to_bool : [< T.cval ] Typed.t -> [> Typed.sbool ] Typed.t Csymex.t

val cast_aggregate_to_bool : Agv.t -> [> Typed.sbool ] Typed.t Csymex.t

type fun_exec =
  args:Agv.t list ->
  (Agv.t, Error.with_trace, State.syn list) InterpM.StateM.Result.t

val get_param_tys : 
  Cerb_frontend.Symbol.sym ->
  Cerb_frontend.Ctype.ctype list Csymex.t

val fold_bindings : 
  AilSyntax.bindings ->
  init:'a ->
  f:('a -> (AilSyntax.ail_identifier * Cerb_frontend.Ctype.ctype) -> 'a) ->
  'a

val try_with_unsupported : (Store.t -> Store.t) -> unit InterpM.t

val attach_bindings : AilSyntax.bindings -> unit InterpM.t

val remove_bindings : AilSyntax.bindings -> unit InterpM.t

val free_bindings : AilSyntax.bindings -> unit InterpM.t

val pp_bindings : AilSyntax.bindings Fmt.t

val remove_and_free_bindings : AilSyntax.bindings -> unit InterpM.t

val mk_store : 
  (Cerb_frontend.Symbol.sym * Ail_tys.ctype * Aggregate_val.t) list ->
  Store.t

val dealloc_store : unit -> unit InterpM.t

val get_stack_address : Ail_tys.sym -> T.sptr Typed.t option InterpM.t

val try_immediate_load : 
  'a AilSyntax.expression ->
  (Aggregate_val.t option, Error.with_trace, State.syn list)
    InterpM.SSM.Result.t

val try_immediate_store : 
  'a AilSyntax.expression ->
  Aggregate_val.t ->
  [> `NotImmediate | `Success ] InterpM.t

val aggregate_of_constant_exn : 
  loc:Cerb_location.t ->
  ty:Ctype.ctype ->
  Ail_tys.constant ->
  Agv.t

val aggregate_of_constant : 
  ty:Ctype.ctype ->
  Ail_tys.constant ->
  Agv.t Csymex.t

val unwrap_expr : 
  Ail_tys.expr ->
  Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.expression_

val cast_basic : 
  old_ty:Ctype.ctype ->
  new_ty:Ctype.ctype ->
  Soteria_c_lib.Typed.T.cval Typed.t ->
  'a Typed.t Csymex.t

val cast : old_ty:Ctype.ctype -> new_ty:Ctype.ctype -> Agv.t -> Agv.t Csymex.t

val equality_check : 
  ty:Ctype.ctype ->
  (Soteria_c_lib.Typed.T.cval Typed.t * Ctype.ctype) ->
  (Soteria_c_lib.Typed.T.cval Typed.t * Ctype.ctype) ->
  [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t InterpM.t

val aggregate_equality_check : 
  ty:Ctype.ctype ->
  (Soteria_c_lib.Typed.T.cval Typed.t Agv.agv * Ctype.ctype) ->
  (Soteria_c_lib.Typed.T.cval Typed.t Agv.agv * Ctype.ctype) ->
  [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t InterpM.t

val arith_add : 
  signed:bool ->
  ([< Soteria_c_lib.Typed.T.cval ] as 'a) Typed.t ->
  'b Typed.t ->
  ([> `NonZero | `Ptr | `Zero ] Soteria__Bv_values__Typed.t,
    Error.with_trace,
    State.syn list)
    InterpM.SSM.Result.t

val arith_sub : 
  signed:bool ->
  [< Soteria_c_lib.Typed.T.cval ] Typed.t ->
  [< Soteria_c_lib.Typed.T.cval ] Typed.t ->
  ([> `NonZero | `Ptr | `Zero ] Soteria__Bv_values__Typed.t,
    Error.with_trace,
    State.syn list)
    InterpM.SSM.Result.t

val arith_mul : 
  signed:bool ->
  [< Soteria_c_lib.Typed.T.cval ] Typed.t ->
  [< Soteria_c_lib.Typed.T.cval ] Typed.t ->
  ([> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t,
    Error.with_trace,
    State.syn list)
    InterpM.SSM.Result.t

val arith : 
  Ctype.ctype ->
  (Soteria_c_lib.Typed.T.cval Typed.t * Ctype.ctype) ->
  AilSyntax.arithmeticOperator ->
  (Soteria_c_lib.Typed.T.cval Typed.t * Ctype.ctype) ->
  [> `Float | `NonZero | `Ptr | `Zero ] Typed.t InterpM.t

val try_immediate_postfix_op : 
  apply_op:
    (Aggregate_val.t ->
      (Aggregate_val.t, Error.with_trace, State.syn list) InterpM.SSM.Result.t) ->
  'a AilSyntax.expression ->
  (Aggregate_val.t option, Error.with_trace, State.syn list)
    InterpM.SSM.Result.t

val ineq_comparison : 
  int_cmp_op:
    ([> Soteria__Bv_values__Typed.T.sint ] Typed.t ->
      [> Soteria__Bv_values__Typed.T.sint ] Typed.t ->
      [< Soteria__Bv_values__Typed.sbool ] Soteria__Bv_values__Typed.t) ->
  float_cmp_op:
    ('a Typed.t ->
      'b Typed.t ->
      [< Soteria__Bv_values__Typed.sbool ] Soteria__Bv_values__Typed.t) ->
  'c Typed.t Agv.agv ->
  'd Typed.t Agv.agv ->
  ([> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t Agv.agv,
    Error.with_trace,
    State.syn list)
    InterpM.SSM.Result.t

module Stmt_exec_result : sig ... end

val resolve_function : 
  Cerb_frontend.GenTypes.genTypeCategory AilSyntax.expression ->
  (fun_exec * Ail_tys.ctype list option * Stubs.Arg_filter.t) InterpM.t

val eval_expr_list : 
  Ail_tys.expr list ->
  (Agv.t list, Error.with_trace, State.syn list) InterpM.SSM.Result.t

val eval_expr : 
  Ail_tys.expr ->
  (Agv.t, Error.with_trace, State.syn list) InterpM.SSM.Result.t

val exec_body : ret_ty:Ctype.ctype option -> Ail_tys.stmt -> Agv.t InterpM.t

val exec_stmt_list : 
  Stmt_exec_result.t ->
  Ail_tys.stmt list ->
  Stmt_exec_result.t InterpM.t

Executing a goto statement, i.e. jumping to a label, returns the result of executing the label's target statement.

val exec_goto : Ail_tys.sym -> Ail_tys.stmt -> Stmt_exec_result.t InterpM.t

val exec_case : T.sint Typed.t -> Ail_tys.stmt -> Stmt_exec_result.t InterpM.t

val exec_stmt : Ail_tys.stmt -> Stmt_exec_result.t InterpM.t

Executing a statement returns an optional value outcome (if a return statement was hit), or

val exec_fun : Ail_tys.fundef -> fun_exec

val init_prog_state : 
  Ail_tys.linked_program ->
  (unit, Error.with_trace, State.syn list) InterpM.StateM.Result.t