Merge pull request MLanguage#89 from lefessan/z-2021-10-28-mlis

Add mlis for AST files

Makefile

@@ -48,7 +48,9 @@ deps:
 format:
 	dune build @fmt --auto-promote | true
 
-build: format
+build: format dune
+
+dune:
 	dune build $(DUNE_OPTIONS)
 
 # Run only in an opam switch with musl and static options activated

dune-project

@@ -28,7 +28,7 @@
   "The Direction G\195\169n\195\169rale des Finances Publiques (DGFiP)\nuses the M language to specify how French taxes are computed\nfrom the characteristics of a fiscal household. This compiler\nparser the M code into a formalized compact intermediate language\nbefore translating it into various backend languages.\n")
  (depends
   (ocaml
-   (and(>= "4.11.2") (< "4.12.0")))
+   (and(>= "4.11.2")))
   (dune
    (and :build))
   (ANSITerminal

mlang.opam

@@ -15,7 +15,7 @@ license: "GPLv3"
 homepage: "https://gitlab.inria.fr/verifisc/mlang"
 bug-reports: "https://gitlab.inria.fr/verifisc/mlang/issues"
 depends: [
-  "ocaml" {>= "4.11.2" & < "4.12.0"}
+  "ocaml" {>= "4.11.2"}
   "dune" {build}
   "ANSITerminal" {= "0.8.2"}
   "re" {= "1.9.0"}

src/mlang/backend_ir/bir.ml

@@ -1,5 +1,5 @@
-(* Copyright (C) 2019-2021-2020 Inria, contributors: Denis Merigoux <[email protected]> Raphël
-   Monat <[email protected]>
+(* Copyright (C) 2019-2021-2020 Inria, contributors: Denis Merigoux <[email protected]>
+   Raphaël Monat <[email protected]>
 
    This program is free software: you can redistribute it and/or modify it under the terms of the
    GNU General Public License as published by the Free Software Foundation, either version 3 of the

src/mlang/backend_ir/bir.mli

@@ -0,0 +1,45 @@
+(* Copyright (C) 2019-2021-2020 Inria, contributors: Denis Merigoux <[email protected]>
+   Raphaël Monat <[email protected]>
+
+   This program is free software: you can redistribute it and/or modify it under the terms of the
+   GNU General Public License as published by the Free Software Foundation, either version 3 of the
+   License, or (at your option) any later version.
+
+   This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without
+   even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+   General Public License for more details.
+
+   You should have received a copy of the GNU General Public License along with this program. If
+   not, see <https://www.gnu.org/licenses/>. *)
+
+type rule_id = Mir.rule_id
+
+module RuleMap = Mir.RuleMap
+
+type rule = { rule_id : rule_id; rule_name : string; rule_stmts : stmt list }
+
+and stmt = stmt_kind Pos.marked
+
+and stmt_kind =
+  | SAssign of Mir.Variable.t * Mir.variable_data
+  | SConditional of Mir.expression * stmt list * stmt list
+  | SVerif of Mir.condition_data
+  | SRuleCall of rule_id
+
+type program = {
+  rules : rule RuleMap.t;
+  statements : stmt list;
+  idmap : Mir.idmap;
+  mir_program : Mir.program;
+  outputs : unit Mir.VariableMap.t;
+}
+
+val get_all_statements : program -> stmt list
+
+val count_instructions : program -> int
+
+val get_assigned_variables : program -> Mir.VariableDict.t
+
+val get_local_variables : program -> unit Mir.LocalVariableMap.t
+
+val remove_empty_conditionals : stmt list -> stmt list

src/mlang/backend_ir/bir_interface.ml

@@ -1,4 +1,4 @@
-(* Copyright (C) 2019-2021 Inria, contributors: Denis Merigoux <[email protected]> Raphël
+(* Copyright (C) 2019-2021 Inria, contributors: Denis Merigoux <[email protected]> Raphaël
    Monat <[email protected]>
 
    This program is free software: you can redistribute it and/or modify it under the terms of the

src/mlang/backend_ir/bir_interface.mli

@@ -1,4 +1,4 @@
-(* Copyright (C) 2019-2021 Inria, contributors: Denis Merigoux <[email protected]> Raphël
+(* Copyright (C) 2019-2021 Inria, contributors: Denis Merigoux <[email protected]> Raphaël
    Monat <[email protected]>
 
    This program is free software: you can redistribute it and/or modify it under the terms of the

src/mlang/backend_ir/format_bir.ml

@@ -1,5 +1,5 @@
-(* Copyright (C) 2019-2021-2020 Inria, contributors: Denis Merigoux <[email protected]> Raphël
-   Monat <[email protected]>
+(* Copyright (C) 2019-2021-2020 Inria, contributors: Denis Merigoux <[email protected]>
+   Raphaël Monat <[email protected]>
 
    This program is free software: you can redistribute it and/or modify it under the terms of the
    GNU General Public License as published by the Free Software Foundation, either version 3 of the

src/mlang/backend_ir/format_bir.mli

@@ -1,5 +1,5 @@
-(* Copyright (C) 2019-2021-2020 Inria, contributors: Denis Merigoux <[email protected]> Raphël
-   Monat <[email protected]>
+(* Copyright (C) 2019-2021-2020 Inria, contributors: Denis Merigoux <[email protected]>
+   Raphaël Monat <[email protected]>
 
    This program is free software: you can redistribute it and/or modify it under the terms of the
    GNU General Public License as published by the Free Software Foundation, either version 3 of the

src/mlang/m_frontend/mparser.mly

@@ -1,7 +1,7 @@
 (*
 Copyright (C) 2019-2021 Inria, contributor:
     Denis Merigoux <[email protected]>
-    Raphël Monat <[email protected]>
+    Raphaël Monat <[email protected]>
 
 This program is free software: you can redistribute it and/or modify
 it under the terms of the GNU General Public License as published by

src/mlang/m_ir/mir.ml

@@ -1,4 +1,4 @@
-(* Copyright (C) 2019-2021 Inria, contributors: Denis Merigoux <[email protected]> Raphël
+(* Copyright (C) 2019-2021 Inria, contributors: Denis Merigoux <[email protected]> Raphaël
    Monat <[email protected]>
 
    This program is free software: you can redistribute it and/or modify it under the terms of the
@@ -59,17 +59,32 @@ let is_candidate_valid (candidate : execution_number) (current : execution_numbe
 let same_execution_number (en1 : execution_number) (en2 : execution_number) : bool =
   en1.rule_number = en2.rule_number && en1.seq_number = en2.seq_number
 
+type variable_id = int
+(** Each variable has an unique ID *)
+
+type variable = {
+  name : string Pos.marked;  (** The position is the variable declaration *)
+  execution_number : execution_number;
+      (** The number associated with the rule of verification condition in which the variable is
+          defined *)
+  alias : string option;  (** Input variable have an alias *)
+  id : variable_id;
+  descr : string Pos.marked;  (** Description taken from the variable declaration *)
+  attributes : (Mast.input_variable_attribute Pos.marked * Mast.literal Pos.marked) list;
+  is_income : bool;
+  is_table : int option;
+}
+
 module Variable = struct
-  type id = int
-  (** Each variable has an unique ID *)
+  type id = variable_id
 
-  type t = {
+  type t = variable = {
     name : string Pos.marked;  (** The position is the variable declaration *)
     execution_number : execution_number;
         (** The number associated with the rule of verification condition in which the variable is
             defined *)
     alias : string option;  (** Input variable have an alias *)
-    id : id;
+    id : variable_id;
     descr : string Pos.marked;  (** Description taken from the variable declaration *)
     attributes : (Mast.input_variable_attribute Pos.marked * Mast.literal Pos.marked) list;
     is_income : bool;
@@ -95,8 +110,11 @@ end
 (** Local variables don't appear in the M source program but can be introduced by let bindings when
     translating to MIR. They should be De Bruijn indices but instead are unique globals identifiers
     out of laziness. *)
+
+type local_variable = { id : int }
+
 module LocalVariable = struct
-  type t = { id : int }
+  type t = local_variable = { id : int }
 
   let counter : int ref = ref 0
 
@@ -166,29 +184,37 @@ module VariableMap = struct
       map
 end
 
+module VariableDictMap = Map.Make (struct
+  type t = Variable.id
+
+  let compare = compare
+end)
+
+type variable_dict = variable VariableDictMap.t
+
 (** Variable dictionary, act as a set but refered by keys *)
 module VariableDict = struct
-  module Map = Map.Make (struct
-    type t = Variable.id
+  type t = variable_dict
 
-    let compare = compare
-  end)
+  let find = VariableDictMap.find
+
+  let filter = VariableDictMap.filter
 
-  include Map
+  let empty = VariableDictMap.empty
 
-  type t = Variable.t Map.t
+  let bindings = VariableDictMap.bindings
 
-  let singleton v = singleton v.Variable.id v
+  let singleton v = VariableDictMap.singleton v.Variable.id v
 
-  let add v t = add v.Variable.id v t
+  let add v t = VariableDictMap.add v.Variable.id v t
 
-  let mem v t = mem v.Variable.id t
+  let mem v t = VariableDictMap.mem v.Variable.id t
 
-  let fold f t acc = fold (fun _ v acc -> f v acc) t acc
+  let fold f t acc = VariableDictMap.fold (fun _ v acc -> f v acc) t acc
 
-  let union t1 t2 = union (fun _ v _ -> Some v) t1 t2
+  let union t1 t2 = VariableDictMap.union (fun _ v _ -> Some v) t1 t2
 
-  let for_all f t = for_all (fun _ v -> f v) t
+  let for_all f t = VariableDictMap.for_all (fun _ v -> f v) t
 end
 
 module VariableSet = Set.Make (Variable)
@@ -343,21 +369,35 @@ end)
 
 (**{1 Verification conditions}*)
 
+type error_descr = {
+  kind : string Pos.marked;
+  major_code : string Pos.marked;
+  minor_code : string Pos.marked;
+  description : string Pos.marked;
+  isisf : string Pos.marked;
+}
 (** Errors are first-class objects *)
 
+type error = {
+  name : string Pos.marked;  (** The position is the variable declaration *)
+  id : int;  (** Each variable has an unique ID *)
+  descr : error_descr;  (** Description taken from the variable declaration *)
+  typ : Mast.error_typ;
+}
+
 module Error = struct
-  type descr = {
+  type descr = error_descr = {
     kind : string Pos.marked;
     major_code : string Pos.marked;
     minor_code : string Pos.marked;
     description : string Pos.marked;
     isisf : string Pos.marked;
   }
 
-  type t = {
+  type t = error = {
     name : string Pos.marked;  (** The position is the variable declaration *)
     id : int;  (** Each variable has an unique ID *)
-    descr : descr;  (** Description taken from the variable declaration *)
+    descr : error_descr;  (** Description taken from the variable declaration *)
     typ : Mast.error_typ;
   }