Merge branch 'main-function-selection-in-bir' into backend-ocaml

Author: mdurero

src/mlang/backend_compilers/bir_to_dgfip_c.ml

@@ -169,7 +169,7 @@ let rec simpl_dexpr (de : dexpr) : dexpr =
       | Done -> Dzero
       | Dlit f when f <> 0. -> Dzero
       | Dzero -> Done
-      | _ -> de
+      | de -> Dunop ("!", de)
     end
   | Dite (dec, det, dee) -> begin
       match (simpl_dexpr dec, simpl_dexpr det, simpl_dexpr dee) with

src/mlang/backend_ir/bir.ml

@@ -153,7 +153,7 @@ let main_statements_with_context (p : program) : stmt list =
       Errors.raise_error
         "This Bir program has no context constants and conditions stored"
 
-let main_statements_with_reset (p : program) : stmt list =
+let main_statements_with_context_and_tgv_init (p : program) : stmt list =
   match p.context with
   | Some context ->
       context.unused_inputs_init_stmts @ main_statements_with_context p

src/mlang/backend_ir/bir.mli

@@ -62,6 +62,23 @@ type program_context = {
   adhoc_specs_conds_stmts : stmt list;
   unused_inputs_init_stmts : stmt list;
 }
+(** This record allows to store statements generated from the m_spec file
+    without modifying the [Bir.program] function map. Thus the map reflects the
+    computation strictly as described in M and MPP.
+
+    Bir module public interface can then provide access to the statements
+    associated with the declared main function either:
+
+    - as defined in M source,
+    - composed with the m_spec constant assignations and conditions,
+    - composed with an initialisation of the variable dictionnary and the m_spec
+      features.
+
+    Initialisation of the variables at the [Bir] level including unused
+    variables is necessary to the [Bir.interpreter] but frowned upon in code
+    generation backends where the data structure size incites to use idiomatic
+    efficient methods of initialisation instead of resting upon a row of
+    assignments. *)
 
 type program = {
   mpp_functions : mpp_function FunctionMap.t;
@@ -93,7 +110,7 @@ val main_statements : program -> stmt list
 
 val main_statements_with_context : program -> stmt list
 
-val main_statements_with_reset : program -> stmt list
+val main_statements_with_context_and_tgv_init : program -> stmt list
 
 val get_all_statements : program -> stmt list
 

src/mlang/backend_ir/bir_instrumentation.ml

@@ -144,4 +144,4 @@ and get_code_locs_stmts (p : Bir.program) (stmts : Bir.stmt list)
   locs
 
 let get_code_locs (p : Bir.program) : code_locs =
-  get_code_locs_stmts p (Bir.main_statements_with_reset p) []
+  get_code_locs_stmts p (Bir.main_statements_with_context_and_tgv_init p) []

src/mlang/backend_ir/bir_interpreter.ml

@@ -753,8 +753,19 @@ module Make (N : Bir_number.NumberInterface) = struct
     try
       let ctx =
         evaluate_stmts p ctx
-          (Bir.main_statements_with_reset p)
+          (Bir.main_statements_with_context_and_tgv_init p)
           [] code_loc_start_value
+        (* For the interpreter to operate properly, all input variables must be
+           declared at some point, even if they aren't used as input (either
+           contextual constants or entered at interpreter prompt). The M program
+           doesn't include default assignation for non-entered input variables,
+           so unused inputs are not declared in the main statements.
+
+           The use of main_statement_with_context_and_tgv_init ensures every
+           variable from the TGV dictionnary is assigned to "undefined" by
+           default, before context statements overload the contextual constants
+           according to the spec file and interpreter prompt assignements
+           overload entered variables. *)
       in
       ctx
     with RuntimeError (e, ctx) ->

src/mlang/backend_ir/format_bir.ml

@@ -74,4 +74,4 @@ let format_rules fmt rules =
 
 let format_program fmt (p : program) =
   Format.fprintf fmt "%a%a" format_rules p.rules_and_verifs format_stmts
-    (Bir.main_statements_with_reset p)
+    (Bir.main_statements_with_context_and_tgv_init p)