[RFC] Add support for the Model Checking Intermediate Language (MCIL) #170

daniel-larraz · 2023-07-03T11:54:28Z

This PR adds MCIL as a version of the smtlib2 language. The current specification of the language can be found here.

Co-authored-by: kian-weimer <[email protected]>

Gbury · 2023-07-03T13:24:58Z

Thank you for the contribution !

I haven't had time to read everything yet, but I already have some questions/remarks:

for the parsing part, I'd rather avoid using an assoc list for the variables (and the conds), and instead have the mk_sys function explicitly take each list separately with a named argument, e.g. : mk_sys : input:var list -> output:var list -> local:var list -> ... ->
it would be nice to have some examples that do pass typing (there are only error examples currently if I'm not mistaken)
I'm wondering whether we really need to have a separate notion of systems: instead, would it be reasonable to make it so that we have a type (or an indexed family of types) 'local system, and have system definitions actually create a constant of type input_var_1_type -> ... -> input_var_n_type -> output_var_1_type -> ... -> output_var_m_type -> (local_var_1_type, ...) system. That would minimize the required amount of new code (but maybe that would result in worse error messages, so it may not be a good solution...)

daniel-larraz · 2023-07-04T11:48:40Z

@Gbury , thank you for your quick feedback.

I addressed your first two points.

I'm not sure about the last point. Unless you feel strongly about that change, I would postpone it.

Gbury · 2023-07-04T15:41:53Z

I'm not sure about the last point. Unless you feel strongly about that change, I would postpone it.

Agreed, ^^

Another question: why add a dedicated command for declaring enumeration (declare-enum-sort) when it can already be done using declare-datatypes ?

daniel-larraz · 2023-07-04T16:02:59Z

Another question: why add a dedicated command for declaring enumeration (declare-enum-sort) when it can already be done using declare-datatypes?

I don't know the answer. I only know that the dedicated command is part of the current MCIL specification. I can ask around to figure out the rationale.

daniel-larraz · 2023-07-17T10:31:13Z

Another question: why add a dedicated command for declaring enumeration (declare-enum-sort) when it can already be done using declare-datatypes?

I don't know the answer. I only know that the dedicated command is part of the current MCIL specification. I can ask around to figure out the rationale.

I asked around. The (declare-enum-sort) command was added because it allows solvers to support enumeration types without having to support the (much more complex) data types.

Gbury

Overall, the code is mostly good. I did a general overview and left comments to address the major design choices (e.g. having the code checking systems in a separate file instead of in thf.ml).

One question I've been pondering is whether we want to keep the name System, as it lacks a bit of context to know exactly what it's referring to (in particular in a context that is otherwise usually used for theorem proving). Maybe something that more explicitly mentions model checking would be better.

Gbury · 2023-07-22T14:44:03Z

src/typecheck/thf.ml

@@ -2527,9 +2551,268 @@ module Make
        ) d.contents
    end

-  (* High-level parsing function *)
+  (* MCIL Only System Definitions and Checks *)
  (* ************************************************************************ *)


I think that most of this new code could actually live in a separate functor and file. This can be done using the get_global_custom and set_global_custom functions to manage the table of defined systems (instead of adding it in the type definition for env). It should not require to change code too much, and makes the model-checking part more independant.

And, in that process of moving that code to another file and functor, you end up needing some functions from thf.ml to be exposed, don't hesitate to add them to the intf.ml file so that they can be accessed from outside.

Gbury · 2023-07-22T14:51:36Z

src/typecheck/thf.ml

+      Was causing errors and its purpose is unknown. *)
+    (* List.iter (check_used_term_var ~kind:`Function_param env) input;
+    List.iter (check_used_term_var ~kind:`Function_param env) output;
+    List.iter (check_used_term_var ~kind:`Function_param env) local; *)


These lines are used to emit warnings in cases when some of the variables are not used. If the warnings emitted are spurious, it may be because the mark_term_var_as_used function was not called at a point where it should have been called.

I put the code back again, and now it works fine.

Gbury · 2023-07-22T14:54:21Z

src/typecheck/thf.ml

+
+    let id, f = id_for_sig ssig_env input output local d in
+
+    (* [Kian] Finalize Def -- What do these do? *)


I'll try and answer what's the use of the functions below, ^^
Additionally, if you could make a list of the functions/places where you think additional documentation would be useful so that I can add it, that'd be great !

Thank you for your explanations! I'll let you know.

Gbury · 2023-07-22T15:01:49Z

src/typecheck/thf.ml

+    (* [Kian] Finalize Def -- What do these do? *)
+
+    (* let def = parse_def ssig t in
+    let ssig = close_wildcards_in_sig ssig t in


This function's goal is to resolve any leftover type constraints.

For more context: in order to accommodate some other languages (e.g. alt-ergo's and zipperposition's native formats), the typechecker can perform some type inference. It does so by creating some type wildcards, which are akin to type "holes" that can be filled in when we unify some types (which happen when typechecking an application of a pattern match for instance). That means that once we get to the top-level of a definition, we have to check that there aren't any "holes" left (and either fill these using a heuristic, or emit errors), and that's the goal of that function.

In addition, some languages (mainly ae's native language) have implicit type quantification, so the close_wildcards_in_sig function can sometimes add some type variables that arise from type inference.

In this case here that should not happen (at least not for now), so I think that instead of that you can simply use the check_no_free_wildcards function.

Gbury · 2023-07-22T15:03:57Z

src/typecheck/thf.ml

+
+    (* [Kian] Finalize Def -- What do these do? *)
+
+    (* let def = parse_def ssig t in


That function is here because in the general case of recursive definitions, you have to first determine the signatures/type/sorts of the defined symbols, add them to the env, and then you can type the definition. In the case of automata systems, I don't think that you can define recursive systems, so the distinction between determining the signature and the actual definition is not needed, and therefore you can just remove this line.

Got it. Thanks!

src/standard/statement.ml

The new code uses the `get_global_custom` and `set_global_custom` functions to manage the table of defined systems, and calls the check_no_free_wildcards function. This commit also removes the system constant that is not necessary anymore. The code that emits warnings for unused variables is enabled again; no issues were found.

Gbury

Apologies for the very late review.

Gbury · 2023-10-04T15:52:52Z

src/loop/typer.ml

+  Report.Error.mk ~code ~mnemonic:"duplicate-definition"
+    ~message:(fun fmt (id, file, old) ->
+        Format.fprintf fmt
+          "Duplicate declaration of %a, which was already defined at %a"


The error name and mnemonic uses definition but the error message here says declaration, is it intentional ? is there a difference between declaration/definition in mcil ?

src/standard/statement.ml

Gbury · 2023-10-04T16:00:25Z

src/standard/statement.mli

@@ -213,3 +243,6 @@ val print_group :
  Format.formatter -> 'a group -> unit
 (* Printer for groups. *)

+val print_def_sys : Format.formatter -> sys_def -> unit
+(* Printer for system definition. *)


print_chk_sys could probably also be exposed here ?

Gbury · 2023-10-04T16:01:49Z

src/typecheck/intf.ml

+  val file : env -> Dolmen.Std.Loc.file
+  (** Get the file for an env. *)
+
+  val add_term_var : env -> Dolmen.Std.Id.t -> term_var -> Dolmen.Std.Term.t -> env


This function (and the two functions after) lack doc comments, tell me if you need me to write these.

Gbury · 2023-10-06T15:21:07Z

src/typecheck/trans_sys.ml

+    | Duplicate_definition : Dolmen.Std.Id.t * Dolmen.Std.Loc.t -> Dolmen.Std.Loc.t Type.err
+
+
+  let key = Dolmen.Std.Tag.create ()


it would be better to rename this to a more informative name, such as sys_definitions

Gbury · 2023-10-26T15:06:07Z

src/typecheck/trans_sys.ml

+    parse_subsystems env d
+
+  let finalize_sys (d : Stmt.sys_def) ((env, _), input, output, local) =
+    Type.check_no_free_wildcards env d.init;


These functions should be called right after typing the corresponding ast. In essence, wildcards are added to the global state stored inside the env, hence why the check_no_free_wildcards should be called right after typing, to ensure that all free wildcards were actually created when typing some ast.

Gbury · 2023-10-26T15:11:23Z

src/typecheck/trans_sys.ml

+    Type.check_no_free_wildcards env d.init;
+    Type.check_no_free_wildcards env d.trans;
+    Type.check_no_free_wildcards env d.inv;
+    let input, output, local = vars input, vars output, vars local in


This way of writing code is a bit mislead I think. Instead I think it'd be better to 'inline' the call to vars for each one of the List.iter below.

Gbury · 2023-10-26T15:18:19Z

src/typecheck/trans_sys.ml

+      if (n1 != n2) then _bad_arity env (Id id) n1 n2 a ;
+      List.iter2
+        (fun (_, v1, _) (_, v2, a2) ->
+          ensure env a2 (Type.T.of_var v2) (Type.T.Var.ty v1)


I think that here it would be better to directly check for equality of the types, and raise an error if the equality does not hold.

Gbury · 2023-10-26T15:22:18Z

src/typecheck/trans_sys.ml

+          if not (M.mem s cond_ids) then
+            Type._error env (Ast ast) (Type.Cannot_find (s, ""));
+        )
+        | _ -> assert false


this should be a proper error, not an assert false

Gbury · 2023-10-26T15:24:13Z

src/typecheck/trans_sys.mli

+  (** Parse a transition system definition *)
+
+  val parse_check : Type.env -> Dolmen.Std.Statement.sys_check -> [> `Sys_check ]
+  (** Parse a transition system check *)


As mentionned in other comments: the current types here (and in parse_def) will lose information (e.g. the transitions in parse_def, and everything in this case), and we should not lose information

Add support for the Model Checking Intermediate Language (MCIL)

c2b4799

Co-authored-by: kian-weimer <[email protected]>

daniel-larraz added 3 commits July 4, 2023 13:40

Make sys_def and sys_check take named arguments instead of assoc list

d4d06b0

Add missing 'expected' files

9fdc946

Add MCIL examples that do pass typing

1ce97e9

Add MCIL examples with enumeration declarations

12fdb81

Gbury requested changes Aug 31, 2023

View reviewed changes

daniel-larraz added 11 commits September 6, 2023 17:01

Remove unused var from MCIL test

1a677a3

Remove unused enum definitions

1aa1bc3

Remove spurious new lines

5a282f2

Move Cannot_find_system exception to MCIL module

124ffa1

Refine undefined-system error location for sys_check

8693e30

Refine and add errors related to subsystems

7b152d3

Update MCIL tests

b746fa6

Add error for unbound identifier in query

67aaf5b

Add duplicate-definition error in MCIL

57ee815

Fix MCIL system_instantiation grammar rule

6576846

daniel-larraz requested a review from Gbury September 15, 2023 02:03

Gbury requested changes Oct 26, 2023

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[RFC] Add support for the Model Checking Intermediate Language (MCIL) #170

[RFC] Add support for the Model Checking Intermediate Language (MCIL) #170

daniel-larraz commented Jul 3, 2023

Gbury commented Jul 3, 2023

daniel-larraz commented Jul 4, 2023 •

edited

Loading

Gbury commented Jul 4, 2023

daniel-larraz commented Jul 4, 2023

daniel-larraz commented Jul 17, 2023

Gbury left a comment

Gbury Jul 22, 2023

Gbury Jul 22, 2023

daniel-larraz Sep 6, 2023

Gbury Jul 22, 2023

daniel-larraz Sep 6, 2023

Gbury Jul 22, 2023

daniel-larraz Sep 6, 2023

Gbury Jul 22, 2023

daniel-larraz Sep 6, 2023

Gbury Jul 22, 2023

daniel-larraz Sep 6, 2023

Gbury left a comment

Gbury Oct 4, 2023

Gbury Oct 4, 2023

Gbury Oct 4, 2023

Gbury Oct 6, 2023

Gbury Oct 26, 2023

Gbury Oct 26, 2023

Gbury Oct 26, 2023

Gbury Oct 26, 2023

Gbury Oct 26, 2023


		let id, f = id_for_sig ssig_env input output local d in

		(* [Kian] Finalize Def -- What do these do? *)


		(* [Kian] Finalize Def -- What do these do? *)

		(* let def = parse_def ssig t in

		\| Duplicate_definition : Dolmen.Std.Id.t * Dolmen.Std.Loc.t -> Dolmen.Std.Loc.t Type.err


		let key = Dolmen.Std.Tag.create ()

[RFC] Add support for the Model Checking Intermediate Language (MCIL) #170

Are you sure you want to change the base?

[RFC] Add support for the Model Checking Intermediate Language (MCIL) #170

Conversation

daniel-larraz commented Jul 3, 2023

Gbury commented Jul 3, 2023

daniel-larraz commented Jul 4, 2023 • edited Loading

Gbury commented Jul 4, 2023

daniel-larraz commented Jul 4, 2023

daniel-larraz commented Jul 17, 2023

Gbury left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Gbury left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

daniel-larraz commented Jul 4, 2023 •

edited

Loading