Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add typing extensions, and the bvconv extension #208

Merged
merged 2 commits into from
Mar 6, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 29 additions & 7 deletions src/bin/options.ml
Original file line number Diff line number Diff line change
Expand Up @@ -268,6 +268,18 @@ let report_style =
]


(* Typing extensions *)
(* ************************************************************************ *)

let typing_extension_list =
List.map
(fun ext -> Loop.Typer.Ext.name ext, ext)
(Loop.Typer.Ext.list ())

let typing_ext =
Arg.enum typing_extension_list


(* Smtlib2 logic and extensions *)
(* ************************************************************************ *)

Expand Down Expand Up @@ -352,10 +364,10 @@ let mk_run_state
time_limit size_limit
response_file
flow_check
header_check header_licenses
header_lang_version
header_check header_licenses header_lang_version
smtlib2_forced_logic smtlib2_exts
type_check check_model (* check_model_mode *)
type_check extension_builtins
check_model (* check_model_mode *)
debug report_style max_warn reports syntax_error_ref
=
(* Side-effects *)
Expand All @@ -380,7 +392,9 @@ let mk_run_state
|> Loop.Parser.init
~syntax_error_ref
~interactive_prompt:Loop.Parser.interactive_prompt_lang
|> Loop.Typer.init ~smtlib2_forced_logic
|> Loop.Typer.init
~smtlib2_forced_logic
~extension_builtins
|> Loop.Typer_Pipe.init ~type_check
|> Loop.Check.init
~check_model
Expand Down Expand Up @@ -613,6 +627,14 @@ let state =
Arg.(value & opt_all smtlib2_ext [] &
info ["internal-smtlib2-extension"] ~docs:internal_section ~doc)
in
let typing_ext =
let doc = Format.asprintf
"Enable typing extensions.
$(docv) must be %s" (Arg.doc_alts_enum typing_extension_list)
in
Arg.(value & opt_all typing_ext [] &
info ["ext"] ~docs ~doc)
in
let debug =
let doc = Format.asprintf
"Activate debug mode. Among other things, this will make dolmen \
Expand Down Expand Up @@ -673,10 +695,10 @@ let state =
time $ size $
response_file $
flow_check $
header_check $ header_licenses $
header_lang_version $
header_check $ header_licenses $ header_lang_version $
force_smtlib2_logic $ smtlib2_extensions $
typing $ check_model $ (* check_model_mode $ *)
typing $ typing_ext $
check_model $ (* check_model_mode $ *)
debug $ report_style $ max_warn $ reports $ syntax_error_ref)


Expand Down
13 changes: 13 additions & 0 deletions src/interface/term.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1368,6 +1368,19 @@ module type Smtlib_Array = sig

end

module type Smtlib_Bvconv = sig

type t
(** The type of terms *)

val to_nat : t -> t
(** Application of the bv2nat conversion function. *)

val of_int : int -> t -> t
(** Application of the int2bv conversion function. *)

end

module type Smtlib_Bitv = sig

type t
Expand Down
81 changes: 65 additions & 16 deletions src/loop/typer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,9 @@ module Smtlib2_Arrays =
module Smtlib2_Bitv =
Dolmen_type.Bitv.Smtlib2.Tff(T)
(Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv)
module Smtlib2_Bvconv =
Dolmen_type.Bitv.Smtlib2.Bvconv(T)
(Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv)
module Smtlib2_Float =
Dolmen_type.Float.Smtlib2.Tff(T)
(Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term)
Expand Down Expand Up @@ -1079,26 +1082,63 @@ module Typer(State : State.S) = struct
| `Response of Response.language
]

(* Extensions builtins *)
(* ************************************************************************ *)

module Ext = struct

type t = {
name : string;
builtins : lang -> T.builtin_symbols;
}

let all = ref []
let list () = !all
let name { name; _ } = name
let builtins { builtins; _ } = builtins

let create ~name ~builtins =
let t = { name; builtins; } in
all := t :: !all;
t

let bv2nat =
create ~name:"bvconv"
~builtins:(function
| `Logic Logic.Smtlib2 version ->
Smtlib2_Bvconv.parse (`Script version)
| _ -> Dolmen_type.Base.noop)

end

(* State setup *)
(* ************************************************************************ *)

let pipe = "Typer"
let ty_state : ty_state State.key =
State.create_key ~pipe "ty_state"
let check_model : bool State.key =
State.create_key ~pipe:"Model" "check_model"
let smtlib2_forced_logic : string option State.key =
State.create_key ~pipe "smtlib2_forced_logic"
let extension_builtins : Ext.t list State.key =
State.create_key ~pipe "extensions_builtins"
let additional_builtins : (state -> lang -> T.builtin_symbols) State.key =
State.create_key ~pipe "additional_builtins"

let init
?ty_state:(ty_state_value=new_state ())
?smtlib2_forced_logic:(smtlib2_forced_logic_value=None)
?extension_builtins:(extension_builtins_value=[])
?additional_builtins:(additional_builtins_value=fun _ _ _ _ -> `Not_found)
st =
st
|> State.set ty_state ty_state_value
|> State.set smtlib2_forced_logic smtlib2_forced_logic_value
|> State.set extension_builtins extension_builtins_value
|> State.set additional_builtins additional_builtins_value


(* Input helpers *)
(* ************************************************************************ *)

Expand Down Expand Up @@ -1450,7 +1490,13 @@ module Typer(State : State.S) = struct
in
raise (State.Error st)
in
let additional_builtins = State.get additional_builtins st st lang in
let user_builtins =
let additional_builtins = State.get additional_builtins st st lang in
let extension_builtins =
List.map (fun ext -> Ext.builtins ext lang) (State.get extension_builtins st)
in
additional_builtins :: extension_builtins
in
match lang with
(* Dimacs & iCNF
- these infer the declarations of their constants
Expand All @@ -1473,7 +1519,10 @@ module Typer(State : State.S) = struct
preferred = Dolmen.Std.Expr.Ty.prop;
});
} in
let builtins = Dimacs.parse in
let builtins = Dolmen_type.Base.merge (
user_builtins @ [
Dimacs.parse
]) in
T.empty_env ~order:First_order
~st:(State.get ty_state st).typer
~var_infer ~sym_infer ~poly
Expand All @@ -1494,13 +1543,13 @@ module Typer(State : State.S) = struct
infer_type_csts = false;
infer_term_csts = No_inference;
} in
let builtins = Dolmen_type.Base.merge [
additional_builtins;
let builtins = Dolmen_type.Base.merge (
user_builtins @ [
Ae_Core.parse;
Ae_Arith.parse;
Ae_Arrays.parse;
Ae_Bitv.parse;
] in
]) in
T.empty_env ~order:First_order
~st:(State.get ty_state st).typer
~var_infer ~sym_infer ~poly
Expand All @@ -1524,11 +1573,11 @@ module Typer(State : State.S) = struct
infer_type_csts = false;
infer_term_csts = No_inference;
} in
let builtins = Dolmen_type.Base.merge [
additional_builtins;
let builtins = Dolmen_type.Base.merge (
user_builtins @ [
Zf_Core.parse;
Zf_arith.parse
] in
]) in
T.empty_env ~order:Higher_order
~st:(State.get ty_state st).typer
~var_infer ~sym_infer ~poly
Expand All @@ -1553,11 +1602,11 @@ module Typer(State : State.S) = struct
infer_type_csts = false;
infer_term_csts = No_inference;
} in
let builtins = Dolmen_type.Base.merge [
additional_builtins;
let builtins = Dolmen_type.Base.merge (
user_builtins @ [
Tptp_Core_Ho.parse v;
Tptp_Arith.parse v;
] in
]) in
T.empty_env ~order:Higher_order
~st:(State.get ty_state st).typer
~var_infer ~sym_infer ~poly
Expand Down Expand Up @@ -1590,11 +1639,11 @@ module Typer(State : State.S) = struct
};
});
} in
let builtins = Dolmen_type.Base.merge [
additional_builtins;
let builtins = Dolmen_type.Base.merge (
user_builtins @ [
Tptp_Core.parse v;
Tptp_Arith.parse v;
] in
]) in
T.empty_env ~order:First_order
~st:(State.get ty_state st).typer
~var_infer ~sym_infer ~poly
Expand Down Expand Up @@ -1640,7 +1689,7 @@ module Typer(State : State.S) = struct
T._error env (Located loc) Missing_smtlib_logic
| Smtlib2 logic ->
let builtins = Dolmen_type.Base.merge (
additional_builtins ::
user_builtins @
builtins_of_smtlib2_logic (`Script v) logic
) in
let quants = logic.features.quantifiers in
Expand Down Expand Up @@ -1674,7 +1723,7 @@ module Typer(State : State.S) = struct
T._error env (Located loc) Missing_smtlib_logic
| Smtlib2 logic ->
let builtins = Dolmen_type.Base.merge (
additional_builtins ::
user_builtins @
builtins_of_smtlib2_logic (`Response v) logic
) in
let quants = logic.features.quantifiers in
Expand Down
64 changes: 49 additions & 15 deletions src/loop/typer_intf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -129,16 +129,6 @@ module type Typer_Full = sig
type builtin_symbols
(** The type of builin symbols for the type-checker. *)

val ty_state : ty_state key
(** Key to store the local typechecking state in the global pipeline state. *)

val check_model : bool key
(** The typechecker needs to know whether we are checking models or not. *)

val smtlib2_forced_logic : string option key
(** Force the typechecker to use the given logic (instead of using the one declared
in the `set-logic` statement). *)

include Typer
with type env := env
and type state := state
Expand All @@ -153,11 +143,48 @@ module type Typer_Full = sig
(** This signature includes the requirements to instantiate the {Pipes.Make:
functor*)

val init :
?ty_state:ty_state ->
?smtlib2_forced_logic:string option ->
?additional_builtins:(state -> lang -> builtin_symbols) ->
state -> state
module Ext : sig
(** Define typing extensions.

These extensions are typically extensions used by some community,
but not yet part of the standard.

@since 0.10 *)

type t
(** The type of typing extensions. *)

val name : t -> string
(** Extension name, sould be suitable for cli options. *)

val builtins : t -> lang -> builtin_symbols
(** Reutnrs the typing builtins from an extension. *)

val create : name:string -> builtins:(lang -> builtin_symbols) -> t
(** Create a new extension. *)

val list : unit -> t list
(** The list of all extensions. *)

val bv2nat : t
(** Typing extension to add the `bv2nat` function. *)

end

val ty_state : ty_state key
(** Key to store the local typechecking state in the global pipeline state. *)

val check_model : bool key
(** The typechecker needs to know whether we are checking models or not. *)

val smtlib2_forced_logic : string option key
(** Force the typechecker to use the given logic (instead of using the one declared
in the `set-logic` statement). *)

val extension_builtins : Ext.t list key
(** Use typing extensions defined by the typechecker.

@since 0.10 *)

val additional_builtins : (state -> lang -> builtin_symbols) key
(** Add new builtin symbols to the typechecker, depending on the current
Expand All @@ -167,6 +194,13 @@ module type Typer_Full = sig

@before 0.9 [additional_builtins] had type [builtin_symbols ref]. *)

val init :
?ty_state:ty_state ->
?smtlib2_forced_logic:string option ->
?extension_builtins:(Ext.t list) ->
?additional_builtins:(state -> lang -> builtin_symbols) ->
state -> state

val report_error : input:input -> state -> error -> state
(** Report a typing error by calling the appropriate state function. *)

Expand Down
2 changes: 2 additions & 0 deletions src/standard/builtin.ml
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,8 @@ type _ t +=
type _ t +=
| Bitv of int
| Bitvec of string
| Bitv_to_nat of { n : int; }
| Bitv_of_int of { n : int; }
| Bitv_concat of { n : int; m : int }
| Bitv_extract of { n : int; i : int; j : int }
| Bitv_repeat of { n : int; k : int }
Expand Down
6 changes: 6 additions & 0 deletions src/standard/builtin.mli
Original file line number Diff line number Diff line change
Expand Up @@ -350,6 +350,12 @@ type _ t +=
(** [Bitvec s: Bitv]: bitvector litteral. The string [s] should
be a binary representation of bitvectors using characters
['0'], and ['1'] (lsb last) *)
| Bitv_to_nat of { n : int; }
(** [Bitv_to_nat(n): Bitv(n) -> Int]:
conversion from bitvectors to integers. *)
| Bitv_of_int of { n : int; }
(** [Bitv_of_int(n): Int -> Bitv(n)]:
conversion fromm (signed) integers to bitvectors. *)
| Bitv_concat of { n : int; m : int }
(** [Bitv_concat(n,m): Bitv(n) -> Bitv(m) -> Bitv(n+m)]:
concatenation operator on bitvectors. *)
Expand Down
Loading
Loading