formalsec / smtml / 536

Committed 02 May 2026 03:27PM UTC coverage: 48.356% (+0.07%) from 48.287%

Build # 536

Build Type

push

github

Committed by

filipeom

Commit Message

Improve failure info in mappings

Coverage Stats

0 of 13 new or added lines in 2 files covered. (0.0%)

51 existing lines in 1 file now uncovered.

2426 of 5017 relevant lines covered (48.36%)

41.13 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

23.31

/src/smtml/dolmenexpr_to_expr.ml

(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2026 formalsec *)
(* Written by Hichem Rami Ait El Hara *)

module DExpr = Dolmen_std.Expr
module DTy = DExpr.Ty
module DTerm = DExpr.Term
module DBuiltin = Dolmen_std.Builtin
module DM = Dolmen_model

module Builtin = struct
  (* additional builtins *)

  let string_ty_cst : DExpr.Term.ty_const =
    DExpr.Id.mk ~builtin:DBuiltin.Base
      (Dolmen_std.Path.global "StringTy")
      DExpr.{ arity = 0; alias = No_alias }

  let string_ty = DTy.apply string_ty_cst []

  let float32_ty = DTy.float 8 24

  let float64_ty = DTy.float 11 53

  let int_to_string : DExpr.term_cst =
    DExpr.Id.mk ~name:"IntToString" ~builtin:DBuiltin.Base
      (Dolmen_std.Path.global "IntToString")
      (DTy.arrow [ DTy.int ] string_ty)

  let string_to_int : DExpr.term_cst =
    DExpr.Id.mk ~name:"StringToInt" ~builtin:DBuiltin.Base
      (Dolmen_std.Path.global "StringToInt")
      (DTy.arrow [ string_ty ] DTy.int)

  let real_to_string : DExpr.term_cst =
    DExpr.Id.mk ~name:"RealToString" ~builtin:DBuiltin.Base
      (Dolmen_std.Path.global "RealToString")
      (DTy.arrow [ DTy.real ] string_ty)

  let string_to_real : DExpr.term_cst =
    DExpr.Id.mk ~name:"StringToReal" ~builtin:DBuiltin.Base
      (Dolmen_std.Path.global "StringToReal")
      (DTy.arrow [ string_ty ] DTy.real)

  let real_to_uint32 : DExpr.term_cst =
    DExpr.Id.mk ~name:"RealToUInt32" ~builtin:DBuiltin.Base
      (Dolmen_std.Path.global "RealToUInt32")
      (DTy.arrow [ DTy.real ] DTy.real)

  let trim_string : DExpr.term_cst =
    DExpr.Id.mk ~name:"TrimString" ~builtin:DBuiltin.Base
      (Dolmen_std.Path.global "TrimString")
      (DTy.arrow [ string_ty ] string_ty)

  let f32_to_string : DExpr.term_cst =
    DExpr.Id.mk ~name:"F32ToString" ~builtin:DBuiltin.Base
      (Dolmen_std.Path.global "F32ToString")
      (DTy.arrow [ float32_ty ] string_ty)

  let string_to_f32 : DExpr.term_cst =
    DExpr.Id.mk ~name:"StringToF32" ~builtin:DBuiltin.Base
      (Dolmen_std.Path.global "StringToF32")
      (DTy.arrow [ string_ty ] float32_ty)

  let f64_to_string : DExpr.term_cst =
    DExpr.Id.mk ~name:"F64ToString" ~builtin:DBuiltin.Base
      (Dolmen_std.Path.global "F64ToString")
      (DTy.arrow [ float64_ty ] string_ty)

  let string_to_f64 : DExpr.term_cst =
    DExpr.Id.mk ~name:"StringToF64" ~builtin:DBuiltin.Base
      (Dolmen_std.Path.global "StringToF64")
      (DTy.arrow [ string_ty ] float64_ty)
end

module DolmenIntf = struct
  include DTerm

  module ConstMap = Map.Make (struct
    type t = DTerm.Const.t

    let compare = DTerm.Const.compare
  end)

  type ty = DTy.t

  type term = DTerm.t

  type interp = DM.Value.t

  type func_decl = DTerm.Const.t

  type model = interp ConstMap.t

  let true_ = DTerm._true

  let false_ = DTerm._false

  let int i = DTerm.Int.mk (string_of_int i)

  let real r = DTerm.Real.mk (string_of_float r)

  let const s ty = DTerm.of_cst (DTerm.Const.mk (Dolmen_std.Path.global s) ty)

  let not_ = DTerm.neg

  let and_ a b = DTerm._and [ a; b ]

  let or_ a b = DTerm._or [ a; b ]

  let implies = DTerm.imply

  let logand = DTerm._and

  let logor = DTerm._or

  let get_vars_from_terms tl =
    List.map
      (fun (t : DTerm.t) ->
        match t.term_descr with
        | Var v -> v
        | _ ->
          Fmt.failwith {|Can't quantify non-variable term "%a"|} DTerm.print t )
      tl

  let forall tl t =
    let tvl = get_vars_from_terms tl in
    DTerm.all ([], tvl) t

  let exists (tl : term list) t =
    let tvl = get_vars_from_terms tl in
    DTerm.ex ([], tvl) t

  let nary_to_binary f tl =
    let rec aux acc = function
      | [] -> acc
      | h :: t -> aux (DTerm.apply_cst f [] [ acc; h ]) t
    in
    match tl with
    | h1 :: h2 :: t -> aux (DTerm.apply_cst f [] [ h1; h2 ]) t
    | _ ->
      Fmt.failwith {|%a applied to less than two terms|} DTerm.Const.print f

  let int_of_term (t : DTerm.t) =
    match t.term_descr with
    | Cst { builtin = DBuiltin.Bitvec i; _ } ->
      (* There may be a proper alternative to int_of_string somewhere,
         since its hidden by prelude. *)
      Z.to_int (Z.of_string i)
    | _ ->
      Fmt.failwith
        {|int_of_term: expected a term that is an integer constant, instead got: %a|}
        DTerm.print t

  module Types = struct
    include DTy

    let regexp = DTy.string_reg_lang

    let ty = DTerm.ty

    let to_ety (ty : DTy.t) : Ty.t =
      match ty with
      | { ty_descr = TyApp ({ builtin = DBuiltin.Int; _ }, _); _ } -> Ty_int
      | { ty_descr = TyApp ({ builtin = DBuiltin.Real; _ }, _); _ } -> Ty_real
      | { ty_descr = TyApp ({ builtin = DBuiltin.Prop; _ }, _); _ } -> Ty_bool
      | { ty_descr =
            TyApp
              ( { builtin = DBuiltin.Base
                ; path = Absolute { name = "StringTy"; _ }
                ; _
                }
              , _ )
        ; _
        } ->
        Ty_str
      | { ty_descr = TyApp ({ builtin = DBuiltin.Bitv n; _ }, _); _ } ->
        Ty_bitv n
      | { ty_descr = TyApp ({ builtin = DBuiltin.Float (8, 24); _ }, _); _ } ->
        Ty_fp 32
      | { ty_descr = TyApp ({ builtin = DBuiltin.Float (11, 53); _ }, _); _ } ->
        Ty_fp 64
      | _ -> Fmt.failwith {|Unsupported dolmen type "%a"|} DTy.print ty
  end

  module Interp = struct
    let to_int interp =
      match DM.Value.extract ~ops:DM.Int.ops interp with
      | Some z -> Z.to_int z
      | _ -> assert false

    let to_real interp =
      match DM.Value.extract ~ops:DM.Real.ops interp with
      | Some q -> Q.to_float q
      | _ -> assert false

    let to_bool interp =
      match DM.Value.extract ~ops:DM.Bool.ops interp with
      | Some b -> b
      | None -> assert false

    let to_string _ = assert false

    let to_bitv interp _n =
      match DM.Value.extract ~ops:DM.Bitv.ops interp with
      | Some z -> z
      | _ -> assert false

    let to_float interp _eb _sb =
      match DM.Value.extract ~ops:DM.Fp.ops interp with
      | Some f -> Farith.F.to_float Farith.Mode.NE f
      | _ -> assert false
  end

  module Int = struct
    include DTerm.Int

    let neg = DTerm.Int.minus

    let to_bv = DTerm.Bitv.of_int

    let mod_ = DTerm.Int.rem_f
  end

  module Real = struct
    include DTerm.Real

    let neg = DTerm.Real.minus
  end

  module String = struct
    include DTerm.String

    let v = DTerm.String.of_ustring

    let to_re = DTerm.String.RegLan.of_string

    let at t ~pos = DTerm.String.at t pos

    let concat = nary_to_binary DTerm.Const.String.concat

    let contains t ~sub = DTerm.String.contains t sub

    let is_prefix t ~prefix = DTerm.String.is_prefix t prefix

    let is_suffix t ~suffix = DTerm.String.is_suffix t suffix

    let le = DTerm.String.leq

    let sub t ~pos ~len = DTerm.String.sub t pos len

    let index_of t ~sub ~pos = DTerm.String.index_of t sub pos

    let last_index_of _t ~sub:_ =
      Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__

    let replace t ~pattern ~with_ = DTerm.String.replace t pattern with_

    let replace_all t ~pattern ~with_ = DTerm.String.replace_all t pattern with_

    let replace_re t ~pattern ~with_ = DTerm.String.replace_re t pattern with_

    let replace_re_all t ~pattern ~with_ =
      DTerm.String.replace_re_all t pattern with_
  end

  module Re = struct
    let all () = DTerm.String.RegLan.all

    let allchar () = DTerm.String.RegLan.allchar

    let none () = DTerm.String.RegLan.empty

    let star = DTerm.String.RegLan.star

    let plus = DTerm.String.RegLan.cross

    let opt = DTerm.String.RegLan.option

    let comp = DTerm.String.RegLan.complement

    let range = DTerm.String.RegLan.range

    let diff = DTerm.String.RegLan.diff

    let inter = DTerm.String.RegLan.inter

    let loop ~min ~max t = DTerm.String.RegLan.loop min max t

    let union = nary_to_binary DTerm.Const.String.Reg_Lang.union

    let concat = nary_to_binary DTerm.Const.String.Reg_Lang.concat
  end

  module Bitv = struct
    include DTerm.Bitv

    let int_to_bitvector (n : Z.t) (bits : int) : string =
      let two_pow_n = Z.shift_left Z.one bits in
      let unsigned_bv = if Z.lt n Z.zero then Z.add two_pow_n n else n in
      let rec to_bitlist acc n bits =
        if bits = 0 then acc
        else
          let bit = Z.(logand n one |> to_string) in
          to_bitlist
            (Smtml_prelude.String.cat bit acc)
            (Z.shift_right n 1) (bits - 1)
      in
      to_bitlist "" unsigned_bv bits

    let v (i : string) (n : int) =
      let bv = int_to_bitvector (Z.of_string i) n in
      DTerm.Bitv.mk bv

    let of_z (v : Z.t) (n : int) = DTerm.Bitv.mk (int_to_bitvector v n)

    let lognot = DTerm.Bitv.not

    let to_int ~signed:_ = DTerm.Bitv.to_nat

    let div = DTerm.Bitv.sdiv

    let div_u = DTerm.Bitv.udiv

    let logor = DTerm.Bitv.or_

    let logand = DTerm.Bitv.and_

    let logxor = DTerm.Bitv.xor

    let shl = DTerm.Bitv.shl

    let ashr = DTerm.Bitv.ashr

    let lshr = DTerm.Bitv.lshr

    let rem = DTerm.Bitv.srem

    let rem_u = DTerm.Bitv.urem

    let rotate_left t1 t2 = DTerm.Bitv.rotate_left (int_of_term t2) t1

    let rotate_right t1 t2 = DTerm.Bitv.rotate_right (int_of_term t2) t1

    let nego _ =
      Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__

    let addo ~signed:_ =
      Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__

    let subo ~signed:_ =
      Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__

    let mulo ~signed:_ =
      Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__

    let divo _ =
      Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__

    let lt = DTerm.Bitv.slt

    let lt_u = DTerm.Bitv.ult

    let le = DTerm.Bitv.sle

    let le_u = DTerm.Bitv.ule

    let gt = DTerm.Bitv.sgt

    let gt_u = DTerm.Bitv.ugt

    let ge = DTerm.Bitv.sge

    let ge_u = DTerm.Bitv.uge

    let extract t ~high ~low = DTerm.Bitv.extract high low t
  end

  module Float = struct
    include DTerm.Float

    module Rounding_mode = struct
      let rne = DTerm.Float.roundNearestTiesToEven

      let rna = DTerm.Float.roundNearestTiesToAway

      let rtp = DTerm.Float.roundTowardPositive

      let rtn = DTerm.Float.roundTowardNegative

      let rtz = DTerm.Float.roundTowardZero
    end

    let v f e s =
      DTerm.Float.real_to_fp e s DTerm.Float.roundTowardZero
        (DTerm.Real.mk (Smtml_prelude.Float.to_string f))

    let sqrt ~rm t = DTerm.Float.sqrt rm t

    let is_normal = DTerm.Float.isNormal

    let is_subnormal = DTerm.Float.isSubnormal

    let is_negative = DTerm.Float.isNegative

    let is_positive = DTerm.Float.isPositive

    let is_infinite = DTerm.Float.isInfinite

    let is_nan = DTerm.Float.isNaN

    let is_zero = DTerm.Float.isZero

    let round_to_integral ~rm t = DTerm.Float.roundToIntegral rm t

    let add ~rm t1 t2 = DTerm.Float.add rm t1 t2

    let sub ~rm t1 t2 = DTerm.Float.sub rm t1 t2

    let mul ~rm t1 t2 = DTerm.Float.mul rm t1 t2

    let div ~rm t1 t2 = DTerm.Float.div rm t1 t2

    let fma ~rm a b c = DTerm.Float.fma rm a b c

    let le = DTerm.Float.leq

    let ge = DTerm.Float.geq

    let to_fp e s ~rm fp = DTerm.Float.to_fp e s rm fp

    let sbv_to_fp e s ~rm bv = DTerm.Float.sbv_to_fp e s rm bv

    let ubv_to_fp e s ~rm bv = DTerm.Float.ubv_to_fp e s rm bv

    let to_ubv n ~rm fp = DTerm.Float.to_ubv n rm fp

    let to_sbv n ~rm fp = DTerm.Float.to_sbv n rm fp

    let of_ieee_bv eb sb bv = DTerm.Float.ieee_format_to_fp eb sb bv

    let to_ieee_bv = None
  end

  module Func = struct
    let make name tyl ty =
      DTerm.Const.mk (Dolmen_std.Path.global name) (DTy.arrow tyl ty)

    let apply f tl = DTerm.apply_cst f [] tl
  end

  module Adt = struct
    module Cons = struct
      type t = Dolmen_std.Path.t * (ty * Dolmen_std.Path.t option) list

      let make _ ~fields:_ = assert false
    end

    type t = DExpr.ty_def * (func_decl * (ty * func_decl option) list) list

    let make cons_name cons =
      let cons_name = DTy.Const.mk (Dolmen_std.Path.local cons_name) 0 in
      DTerm.define_adt cons_name [] cons

    let ty _ = assert false

    let constructor _ = assert false

    let selector _ = assert false

    let tester _ = assert false
  end

  module Smtlib = struct
    let pp ?name:_ ?logic:_ ?status:_ = Fmt.list DTerm.print
  end

  module Model = struct
    let tcst_to_symbol (c : DTerm.Const.t) : Symbol.t =
      match c with
      | { builtin = DBuiltin.Base
        ; path = Local { name } | Absolute { name; _ }
        ; id_ty
        ; _
        } ->
        Symbol.make (Types.to_ety id_ty) name
      | _ ->
        Fmt.failwith {|Unsupported constant term "%a"|} DExpr.Print.term_cst c

    let get_defval (c : DTerm.Const.t) : DM.Value.t =
      match DTerm.Const.ty c with
      | { ty_descr = TyApp ({ builtin = DBuiltin.Int; _ }, _); _ } ->
        DM.Int.mk Z.zero
      | { ty_descr = TyApp ({ builtin = DBuiltin.Real; _ }, _); _ } ->
        DM.Real.mk Q.zero
      | { ty_descr = TyApp ({ builtin = DBuiltin.Prop; _ }, _); _ } ->
        DM.Bool.mk false
      | { ty_descr = TyApp ({ builtin = DBuiltin.Bitv n; _ }, _); _ } ->
        DM.Bitv.mk n Z.zero
      | { ty_descr = TyApp ({ builtin = DBuiltin.Float _; _ }, _); _ } ->
        DM.Fp.mk (Farith.F.of_float 0.)
      | _ -> assert false

    let get_symbols (m : model) =
      ConstMap.fold (fun tcst _ acc -> tcst_to_symbol tcst :: acc) m []

    let eval ?(ctx = Symbol.Map.empty) ?completion:_ (m : model) (e : term) :
      interp option =
      let m =
        ConstMap.fold (fun c v acc -> DM.Model.Cst.add c v acc) m DM.Model.empty
      in
      let m =
        Symbol.Map.fold
          (fun _ (t : term) acc ->
            match t with
            | { term_descr = Cst c; _ } -> (
              match DM.Model.Cst.find_opt c acc with
              | Some _ -> acc
              | None -> DM.Model.Cst.add c (get_defval c) acc )
            | _ -> assert false )
          ctx m
      in
      let env =
        DM.Env.mk m
          ~builtins:
            (DM.Eval.builtins
               [ DM.Core.builtins
               ; DM.Bool.builtins
               ; DM.Int.builtins
               ; DM.Rat.builtins
               ; DM.Real.builtins
               ; DM.Bitv.builtins
               ; DM.Fp.builtins
               ] )
      in
      let v = DM.Eval.eval env e in
      Some v
  end
end

1	(* SPDX-License-Identifier: MIT *)
2	(* Copyright (C) 2023-2026 formalsec *)
3	(* Written by Hichem Rami Ait El Hara *)
4
5	module DExpr = Dolmen_std.Expr
6	module DTy = DExpr.Ty
7	module DTerm = DExpr.Term
8	module DBuiltin = Dolmen_std.Builtin
9	module DM = Dolmen_model
10
11	module Builtin = struct
12	(* additional builtins *)
13
14	let string_ty_cst : DExpr.Term.ty_const =
15	DExpr.Id.mk ~builtin:DBuiltin.Base	28✔
16	(Dolmen_std.Path.global "StringTy")	28✔
17	DExpr.{ arity = 0; alias = No_alias }
18
19	let string_ty = DTy.apply string_ty_cst []	28✔
20
21	let float32_ty = DTy.float 8 24	28✔
22
23	let float64_ty = DTy.float 11 53	28✔
24
25	let int_to_string : DExpr.term_cst =
26	DExpr.Id.mk ~name:"IntToString" ~builtin:DBuiltin.Base	28✔
27	(Dolmen_std.Path.global "IntToString")	28✔
28	(DTy.arrow [ DTy.int ] string_ty)	28✔
29
30	let string_to_int : DExpr.term_cst =
31	DExpr.Id.mk ~name:"StringToInt" ~builtin:DBuiltin.Base	28✔
32	(Dolmen_std.Path.global "StringToInt")	28✔
33	(DTy.arrow [ string_ty ] DTy.int)	28✔
34
35	let real_to_string : DExpr.term_cst =
36	DExpr.Id.mk ~name:"RealToString" ~builtin:DBuiltin.Base	28✔
37	(Dolmen_std.Path.global "RealToString")	28✔
38	(DTy.arrow [ DTy.real ] string_ty)	28✔
39
40	let string_to_real : DExpr.term_cst =
41	DExpr.Id.mk ~name:"StringToReal" ~builtin:DBuiltin.Base	28✔
42	(Dolmen_std.Path.global "StringToReal")	28✔
43	(DTy.arrow [ string_ty ] DTy.real)	28✔
44
45	let real_to_uint32 : DExpr.term_cst =
46	DExpr.Id.mk ~name:"RealToUInt32" ~builtin:DBuiltin.Base	28✔
47	(Dolmen_std.Path.global "RealToUInt32")	28✔
48	(DTy.arrow [ DTy.real ] DTy.real)	28✔
49
50	let trim_string : DExpr.term_cst =
51	DExpr.Id.mk ~name:"TrimString" ~builtin:DBuiltin.Base	28✔
52	(Dolmen_std.Path.global "TrimString")	28✔
53	(DTy.arrow [ string_ty ] string_ty)	28✔
54
55	let f32_to_string : DExpr.term_cst =
56	DExpr.Id.mk ~name:"F32ToString" ~builtin:DBuiltin.Base	28✔
57	(Dolmen_std.Path.global "F32ToString")	28✔
58	(DTy.arrow [ float32_ty ] string_ty)	28✔
59
60	let string_to_f32 : DExpr.term_cst =
61	DExpr.Id.mk ~name:"StringToF32" ~builtin:DBuiltin.Base	28✔
62	(Dolmen_std.Path.global "StringToF32")	28✔
63	(DTy.arrow [ string_ty ] float32_ty)	28✔
64
65	let f64_to_string : DExpr.term_cst =
66	DExpr.Id.mk ~name:"F64ToString" ~builtin:DBuiltin.Base	28✔
67	(Dolmen_std.Path.global "F64ToString")	28✔
68	(DTy.arrow [ float64_ty ] string_ty)	28✔
69
70	let string_to_f64 : DExpr.term_cst =
71	DExpr.Id.mk ~name:"StringToF64" ~builtin:DBuiltin.Base	28✔
72	(Dolmen_std.Path.global "StringToF64")	28✔
73	(DTy.arrow [ string_ty ] float64_ty)	28✔
74	end
75
76	module DolmenIntf = struct
77	include DTerm
78
79	module ConstMap = Map.Make (struct
80	type t = DTerm.Const.t
81
82	let compare = DTerm.Const.compare
83	end)
84
85	type ty = DTy.t
86
87	type term = DTerm.t
88
89	type interp = DM.Value.t
90
91	type func_decl = DTerm.Const.t
92
93	type model = interp ConstMap.t
94
95	let true_ = DTerm._true
96
97	let false_ = DTerm._false
98
99	let int i = DTerm.Int.mk (string_of_int i)	×
100
101	let real r = DTerm.Real.mk (string_of_float r)	×
102
103	let const s ty = DTerm.of_cst (DTerm.Const.mk (Dolmen_std.Path.global s) ty)	×
104
105	let not_ = DTerm.neg
106
107	let and_ a b = DTerm._and [ a; b ]	×
108
109	let or_ a b = DTerm._or [ a; b ]	×
110
111	let implies = DTerm.imply
112
113	let logand = DTerm._and
114
115	let logor = DTerm._or
116
117	let get_vars_from_terms tl =
118	List.map	×
119	(fun (t : DTerm.t) ->
120	match t.term_descr with	×
121	\| Var v -> v	×
122	\| _ ->	×
123	Fmt.failwith {\|Can't quantify non-variable term "%a"\|} DTerm.print t )
124	tl
125
126	let forall tl t =
127	let tvl = get_vars_from_terms tl in	×
128	DTerm.all ([], tvl) t	×
129
130	let exists (tl : term list) t =
131	let tvl = get_vars_from_terms tl in	×
132	DTerm.ex ([], tvl) t	×
133
134	let nary_to_binary f tl =
135	let rec aux acc = function	×
136	\| [] -> acc	×
137	\| h :: t -> aux (DTerm.apply_cst f [] [ acc; h ]) t	×
138	in
139	match tl with
140	\| h1 :: h2 :: t -> aux (DTerm.apply_cst f [] [ h1; h2 ]) t	×
141	\| _ ->	×
142	Fmt.failwith {\|%a applied to less than two terms\|} DTerm.Const.print f
143
144	let int_of_term (t : DTerm.t) =
145	match t.term_descr with	×
146	\| Cst { builtin = DBuiltin.Bitvec i; _ } ->	×
147	(* There may be a proper alternative to int_of_string somewhere,
148	since its hidden by prelude. *)
149	Z.to_int (Z.of_string i)	×
150	\| _ ->	×
151	Fmt.failwith
152	{\|int_of_term: expected a term that is an integer constant, instead got: %a\|}
153	DTerm.print t
154
155	module Types = struct
156	include DTy
157
158	let regexp = DTy.string_reg_lang
159
160	let ty = DTerm.ty
161
162	let to_ety (ty : DTy.t) : Ty.t =
163	match ty with	×
164	\| { ty_descr = TyApp ({ builtin = DBuiltin.Int; _ }, _); _ } -> Ty_int	×
165	\| { ty_descr = TyApp ({ builtin = DBuiltin.Real; _ }, _); _ } -> Ty_real	×
166	\| { ty_descr = TyApp ({ builtin = DBuiltin.Prop; _ }, _); _ } -> Ty_bool	×
167	\| { ty_descr =	×
168	TyApp
169	( { builtin = DBuiltin.Base
170	; path = Absolute { name = "StringTy"; _ }
171	; _
172	}
173	, _ )
174	; _
175	} ->
176	Ty_str
177	\| { ty_descr = TyApp ({ builtin = DBuiltin.Bitv n; _ }, _); _ } ->	×
178	Ty_bitv n
179	\| { ty_descr = TyApp ({ builtin = DBuiltin.Float (8, 24); _ }, _); _ } ->	×
180	Ty_fp 32
181	\| { ty_descr = TyApp ({ builtin = DBuiltin.Float (11, 53); _ }, _); _ } ->	×
182	Ty_fp 64
183	\| _ -> Fmt.failwith {\|Unsupported dolmen type "%a"\|} DTy.print ty	×
184	end
185
186	module Interp = struct
187	let to_int interp =
188	match DM.Value.extract ~ops:DM.Int.ops interp with	×
189	\| Some z -> Z.to_int z	×
190	\| _ -> assert false
191
192	let to_real interp =
193	match DM.Value.extract ~ops:DM.Real.ops interp with	×
194	\| Some q -> Q.to_float q	×
195	\| _ -> assert false
196
197	let to_bool interp =
198	match DM.Value.extract ~ops:DM.Bool.ops interp with	×
199	\| Some b -> b	×
200	\| None -> assert false
201
202	let to_string _ = assert false	×
203
204	let to_bitv interp _n =
205	match DM.Value.extract ~ops:DM.Bitv.ops interp with	×
206	\| Some z -> z	×
207	\| _ -> assert false
208
209	let to_float interp _eb _sb =
210	match DM.Value.extract ~ops:DM.Fp.ops interp with	×
211	\| Some f -> Farith.F.to_float Farith.Mode.NE f	×
212	\| _ -> assert false
213	end
214
215	module Int = struct
216	include DTerm.Int
217
218	let neg = DTerm.Int.minus
219
220	let to_bv = DTerm.Bitv.of_int
221
222	let mod_ = DTerm.Int.rem_f
223	end
224
225	module Real = struct
226	include DTerm.Real
227
228	let neg = DTerm.Real.minus
229	end
230
231	module String = struct
232	include DTerm.String
233
234	let v = DTerm.String.of_ustring
235
236	let to_re = DTerm.String.RegLan.of_string
237
238	let at t ~pos = DTerm.String.at t pos	×
239
240	let concat = nary_to_binary DTerm.Const.String.concat	28✔
241
242	let contains t ~sub = DTerm.String.contains t sub	×
243
244	let is_prefix t ~prefix = DTerm.String.is_prefix t prefix	×
245
246	let is_suffix t ~suffix = DTerm.String.is_suffix t suffix	×
247
248	let le = DTerm.String.leq
249
250	let sub t ~pos ~len = DTerm.String.sub t pos len	×
251
252	let index_of t ~sub ~pos = DTerm.String.index_of t sub pos	×
253
254	let last_index_of _t ~sub:_ =
NEW 255	Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__	×
256
257	let replace t ~pattern ~with_ = DTerm.String.replace t pattern with_	×
258
259	let replace_all t ~pattern ~with_ = DTerm.String.replace_all t pattern with_	×
260
261	let replace_re t ~pattern ~with_ = DTerm.String.replace_re t pattern with_	×
262
263	let replace_re_all t ~pattern ~with_ =
264	DTerm.String.replace_re_all t pattern with_	×
265	end
266
267	module Re = struct
268	let all () = DTerm.String.RegLan.all	×
269
270	let allchar () = DTerm.String.RegLan.allchar	×
271
272	let none () = DTerm.String.RegLan.empty	×
273
274	let star = DTerm.String.RegLan.star
275
276	let plus = DTerm.String.RegLan.cross
277
278	let opt = DTerm.String.RegLan.option
279
280	let comp = DTerm.String.RegLan.complement
281
282	let range = DTerm.String.RegLan.range
283
284	let diff = DTerm.String.RegLan.diff
285
286	let inter = DTerm.String.RegLan.inter
287
288	let loop ~min ~max t = DTerm.String.RegLan.loop min max t	×
289
290	let union = nary_to_binary DTerm.Const.String.Reg_Lang.union	28✔
291
292	let concat = nary_to_binary DTerm.Const.String.Reg_Lang.concat	28✔
293	end
294
295	module Bitv = struct
296	include DTerm.Bitv
297
298	let int_to_bitvector (n : Z.t) (bits : int) : string =
299	let two_pow_n = Z.shift_left Z.one bits in	×
300	let unsigned_bv = if Z.lt n Z.zero then Z.add two_pow_n n else n in	×
301	let rec to_bitlist acc n bits =
302	if bits = 0 then acc	×
303	else
304	let bit = Z.(logand n one \|> to_string) in	×
305	to_bitlist
306	(Smtml_prelude.String.cat bit acc)	×
307	(Z.shift_right n 1) (bits - 1)	×
308	in
309	to_bitlist "" unsigned_bv bits
310
311	let v (i : string) (n : int) =
312	let bv = int_to_bitvector (Z.of_string i) n in	×
313	DTerm.Bitv.mk bv	×
314
315	let of_z (v : Z.t) (n : int) = DTerm.Bitv.mk (int_to_bitvector v n)	×
316
317	let lognot = DTerm.Bitv.not
318
319	let to_int ~signed:_ = DTerm.Bitv.to_nat	×
320
321	let div = DTerm.Bitv.sdiv
322
323	let div_u = DTerm.Bitv.udiv
324
325	let logor = DTerm.Bitv.or_
326
327	let logand = DTerm.Bitv.and_
328
329	let logxor = DTerm.Bitv.xor
330
331	let shl = DTerm.Bitv.shl
332
333	let ashr = DTerm.Bitv.ashr
334
335	let lshr = DTerm.Bitv.lshr
336
337	let rem = DTerm.Bitv.srem
338
339	let rem_u = DTerm.Bitv.urem
340
341	let rotate_left t1 t2 = DTerm.Bitv.rotate_left (int_of_term t2) t1	×
342
343	let rotate_right t1 t2 = DTerm.Bitv.rotate_right (int_of_term t2) t1	×
344
345	let nego _ =
NEW 346	Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__	×
347
348	let addo ~signed:_ =
NEW 349	Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__	×
350
351	let subo ~signed:_ =
NEW 352	Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__	×
353
354	let mulo ~signed:_ =
NEW 355	Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__	×
356
357	let divo _ =
NEW 358	Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ __FUNCTION__	×
359
360	let lt = DTerm.Bitv.slt
361
362	let lt_u = DTerm.Bitv.ult
363
364	let le = DTerm.Bitv.sle
365
366	let le_u = DTerm.Bitv.ule
367
368	let gt = DTerm.Bitv.sgt
369
370	let gt_u = DTerm.Bitv.ugt
371
372	let ge = DTerm.Bitv.sge
373
374	let ge_u = DTerm.Bitv.uge
375
376	let extract t ~high ~low = DTerm.Bitv.extract high low t	×
377	end
378
379	module Float = struct
380	include DTerm.Float
381
382	module Rounding_mode = struct
383	let rne = DTerm.Float.roundNearestTiesToEven
384
385	let rna = DTerm.Float.roundNearestTiesToAway
386
387	let rtp = DTerm.Float.roundTowardPositive
388
389	let rtn = DTerm.Float.roundTowardNegative
390
391	let rtz = DTerm.Float.roundTowardZero
392	end
393
394	let v f e s =
395	DTerm.Float.real_to_fp e s DTerm.Float.roundTowardZero	×
396	(DTerm.Real.mk (Smtml_prelude.Float.to_string f))	×
397
398	let sqrt ~rm t = DTerm.Float.sqrt rm t	×
399
400	let is_normal = DTerm.Float.isNormal
401
402	let is_subnormal = DTerm.Float.isSubnormal
403
404	let is_negative = DTerm.Float.isNegative
405
406	let is_positive = DTerm.Float.isPositive
407
408	let is_infinite = DTerm.Float.isInfinite
409
410	let is_nan = DTerm.Float.isNaN
411
412	let is_zero = DTerm.Float.isZero
413
414	let round_to_integral ~rm t = DTerm.Float.roundToIntegral rm t	×
415
416	let add ~rm t1 t2 = DTerm.Float.add rm t1 t2	×
417
418	let sub ~rm t1 t2 = DTerm.Float.sub rm t1 t2	×
419
420	let mul ~rm t1 t2 = DTerm.Float.mul rm t1 t2	×
421
422	let div ~rm t1 t2 = DTerm.Float.div rm t1 t2	×
423
424	let fma ~rm a b c = DTerm.Float.fma rm a b c	×
425
426	let le = DTerm.Float.leq
427
428	let ge = DTerm.Float.geq
429
430	let to_fp e s ~rm fp = DTerm.Float.to_fp e s rm fp	×
431
432	let sbv_to_fp e s ~rm bv = DTerm.Float.sbv_to_fp e s rm bv	×
433
434	let ubv_to_fp e s ~rm bv = DTerm.Float.ubv_to_fp e s rm bv	×
435
436	let to_ubv n ~rm fp = DTerm.Float.to_ubv n rm fp	×
437
438	let to_sbv n ~rm fp = DTerm.Float.to_sbv n rm fp	×
439
440	let of_ieee_bv eb sb bv = DTerm.Float.ieee_format_to_fp eb sb bv	×
441
442	let to_ieee_bv = None
443	end
444
445	module Func = struct
446	let make name tyl ty =
447	DTerm.Const.mk (Dolmen_std.Path.global name) (DTy.arrow tyl ty)	×
448
449	let apply f tl = DTerm.apply_cst f [] tl	×
450	end
451
452	module Adt = struct
453	module Cons = struct
454	type t = Dolmen_std.Path.t * (ty * Dolmen_std.Path.t option) list
455
456	let make _ ~fields:_ = assert false	×
457	end
458
459	type t = DExpr.ty_def * (func_decl * (ty * func_decl option) list) list
460
461	let make cons_name cons =
462	let cons_name = DTy.Const.mk (Dolmen_std.Path.local cons_name) 0 in	×
463	DTerm.define_adt cons_name [] cons	×
464
465	let ty _ = assert false	×
466
467	let constructor _ = assert false	×
468
469	let selector _ = assert false	×
470
471	let tester _ = assert false	×
472	end
473
474	module Smtlib = struct
475	let pp ?name:_ ?logic:_ ?status:_ = Fmt.list DTerm.print	×
476	end
477
478	module Model = struct
479	let tcst_to_symbol (c : DTerm.Const.t) : Symbol.t =
480	match c with	×
481	\| { builtin = DBuiltin.Base	×
482	; path = Local { name } \| Absolute { name; _ }	×
483	; id_ty
484	; _
485	} ->
486	Symbol.make (Types.to_ety id_ty) name	×
487	\| _ ->	×
488	Fmt.failwith {\|Unsupported constant term "%a"\|} DExpr.Print.term_cst c
489
490	let get_defval (c : DTerm.Const.t) : DM.Value.t =
491	match DTerm.Const.ty c with	×
492	\| { ty_descr = TyApp ({ builtin = DBuiltin.Int; _ }, _); _ } ->	×
493	DM.Int.mk Z.zero
494	\| { ty_descr = TyApp ({ builtin = DBuiltin.Real; _ }, _); _ } ->	×
495	DM.Real.mk Q.zero
496	\| { ty_descr = TyApp ({ builtin = DBuiltin.Prop; _ }, _); _ } ->	×
497	DM.Bool.mk false
498	\| { ty_descr = TyApp ({ builtin = DBuiltin.Bitv n; _ }, _); _ } ->	×
499	DM.Bitv.mk n Z.zero
500	\| { ty_descr = TyApp ({ builtin = DBuiltin.Float _; _ }, _); _ } ->	×
501	DM.Fp.mk (Farith.F.of_float 0.)	×
502	\| _ -> assert false
503
504	let get_symbols (m : model) =
505	ConstMap.fold (fun tcst _ acc -> tcst_to_symbol tcst :: acc) m []	×
506
507	let eval ?(ctx = Symbol.Map.empty) ?completion:_ (m : model) (e : term) :	×
508	interp option =
509	let m =	×
510	ConstMap.fold (fun c v acc -> DM.Model.Cst.add c v acc) m DM.Model.empty	×
511	in
512	let m =	×
513	Symbol.Map.fold
514	(fun _ (t : term) acc ->
515	match t with	×
516	\| { term_descr = Cst c; _ } -> (	×
517	match DM.Model.Cst.find_opt c acc with
518	\| Some _ -> acc	×
519	\| None -> DM.Model.Cst.add c (get_defval c) acc )	×
520	\| _ -> assert false )
521	ctx m
522	in
523	let env =	×
524	DM.Env.mk m
525	~builtins:
526	(DM.Eval.builtins	×
527	[ DM.Core.builtins
528	; DM.Bool.builtins
529	; DM.Int.builtins
530	; DM.Rat.builtins
531	; DM.Real.builtins
532	; DM.Bitv.builtins
533	; DM.Fp.builtins
534	] )
535	in
536	let v = DM.Eval.eval env e in	×
537	Some v	×
538	end
539	end

formalsec / smtml / 536

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous