diff --git a/irj_checker.opam b/irj_checker.opam index 619747f92..f65093f54 100644 --- a/irj_checker.opam +++ b/irj_checker.opam @@ -1,6 +1,6 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" -version: "%%VERSION%%" +version: "186-15-ga4a1d1ff" synopsis: "IRJ test validation tool" description: "This standalone module performs a syntactic validation of the DGFiP IRJ test format" @@ -11,12 +11,12 @@ homepage: "https://github.com/MLanguage/mlang" bug-reports: "https://github.com/MLanguage/mlang/issues" depends: [ "ocaml" {>= "4.11.2"} - "dune" {>= "2.7" & build} + "dune" {build} "odoc" {>= "1.5.3"} "ocamlformat" {= "0.24.1"} ] build: [ - ["dune" "subst"] {dev} + ["dune" "subst"] {pinned} [ "dune" "build" diff --git a/mlang.opam b/mlang.opam index f82831209..12afa4f76 100644 --- a/mlang.opam +++ b/mlang.opam @@ -1,6 +1,6 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" -version: "%%VERSION%%" +version: "186-15-ga4a1d1ff" synopsis: "Compiler for DGFiP's M language" description: """ The Direction Générale des Finances Publiques (DGFiP) @@ -16,7 +16,7 @@ homepage: "https://github.com/MLanguage/mlang" bug-reports: "https://github.com/MLanguage/mlang/issues" depends: [ "ocaml" {>= "4.13.0"} - "dune" {>= "2.7" & build} + "dune" {build} "ANSITerminal" {= "0.8.2"} "cmdliner" {= "1.3.0"} "re" {= "1.11.0"} @@ -29,7 +29,7 @@ depends: [ "parmap" {= "1.2.3"} ] build: [ - ["dune" "subst"] {dev} + ["dune" "subst"] {pinned} [ "dune" "build" diff --git a/src/mlang/backend_compilers/decoupledExpr.ml b/src/mlang/backend_compilers/decoupledExpr.ml index 7cbcfaa9c..5baf53a96 100644 --- a/src/mlang/backend_compilers/decoupledExpr.ml +++ b/src/mlang/backend_compilers/decoupledExpr.ml @@ -313,10 +313,7 @@ let comp op (e1 : constr) (e2 : constr) (stacks : local_stacks) let comp (o : Com.comp_op) = match (e1, e2) with | Dlit f1, Dlit f2 -> - if - Mir_interpreter.FloatDefInterp.compare_numbers o - (Mir_number.RegularFloatNumber.of_float f1) - (Mir_number.RegularFloatNumber.of_float f2) + if Mir_number.RegularFloatNumber.(compare o (of_float f1) (of_float f2)) then Dtrue else Dfalse | Dvar v1, Dvar v2 -> diff --git a/src/mlang/driver.ml b/src/mlang/driver.ml index 08c77b19e..c611dada3 100644 --- a/src/mlang/driver.ml +++ b/src/mlang/driver.ml @@ -131,7 +131,6 @@ let parse () = m_program let run_single_test m_program test = - Mir_interpreter.repl_debug := true; Test_interpreter.check_one_test m_program test !Config.value_sort !Config.round_ops; Cli.result_print "Test passed!" diff --git a/src/mlang/dune b/src/mlang/dune index 0e489f79d..9b9ce6aa4 100644 --- a/src/mlang/dune +++ b/src/mlang/dune @@ -3,7 +3,7 @@ (flags (:standard -open Utils)) (libraries re ANSITerminal parmap cmdliner threads dune-build-info num gmp - menhirLib m_frontend m_ir irj_utils backend_compilers)) + menhirLib m_frontend m_ir irj_utils backend_compilers m_interpreter)) (documentation (package mlang) diff --git a/src/mlang/index.mld b/src/mlang/index.mld index 8d409e935..f44b35a40 100644 --- a/src/mlang/index.mld +++ b/src/mlang/index.mld @@ -28,10 +28,25 @@ and basically all programs typecheck ; however {!module: Mlang.M_frontend.Valida Mlang.M_ir.Com Mlang.M_ir.Format_mir Mlang.M_ir.Mir - Mlang.M_ir.Mir_interpreter Mlang.M_ir.Mir_number Mlang.M_ir.Mir_roundops } +{1 Interpreter} + +The intepreter is the reference for the M semantics. The C code Mlang generates must +follow it. +The main interpreter module is {!module: Mlang.Mir_interpreter.Eval} which defines two +functions: {!Mlang.Mir_interpreter.Eval.evaluate_program} and {!Mlang.Mir_interpreter.Eval.evaluate_expr}. It also defines several modules that evaluates programs and expression +with different float precisions. + +{!modules: + Mlang.Mir_interpreter.Anomalies + Mlang.Mir_interpreter.Context + Mlang.Mir_interpreter.Eval + Mlang.Mir_interpreter.Functions + Mlang.Mir_interpreter.Print + Mlang.Mir_interpreter.Types } + {1 Testing} Mlang comes with a testing framework for M programs that is based on diff --git a/src/mlang/m_ir/mir.mli b/src/mlang/m_ir/mir.mli index a47559704..4f7f938cd 100644 --- a/src/mlang/m_ir/mir.mli +++ b/src/mlang/m_ir/mir.mli @@ -22,14 +22,13 @@ - Constants have been inlined. - Loops (FunCallLoop, Loop) have been unrolled. - Chaining, domain and verification calculations have been unified into - Target calculations. - This filtering is performed by {!M_frontend.Expander}, {!M_frontend.Validator} and - {!M_frontend.Mast_to_mir}. + Target calculations. This filtering is performed by + {!M_frontend.Expander}, {!M_frontend.Validator} and + {!M_frontend.Mast_to_mir}. - The structural difference between {!M_frontend.Mast} and Mir common types are - the replacement of {!Mir.Com.m_var_name} by {!M_ir.Com.Var.t} and - {!M_frontend.Mast.error_name} by {!M_ir.Com.Error.t}. - *) + The structural difference between {!M_frontend.Mast} and Mir common types + are the replacement of {!Mir.Com.m_var_name} by {!M_ir.Com.Var.t} and + {!M_frontend.Mast.error_name} by {!M_ir.Com.Error.t}. *) type set_value = Com.Var.t Com.set_value @@ -64,8 +63,7 @@ type stats = { max_nb_args : int; table_map : Com.Var.t IntMap.t; } -(** A set of constants relative to the program and its selected - applications. *) +(** A set of constants relative to the program and its selected applications. *) type program = { program_safe_prefix : string; diff --git a/src/mlang/m_ir/mir_interpreter.ml b/src/mlang/m_ir/mir_interpreter.ml deleted file mode 100644 index 973164584..000000000 --- a/src/mlang/m_ir/mir_interpreter.ml +++ /dev/null @@ -1,1486 +0,0 @@ -(* Copyright (C) 2019-2021 Inria, contributor: Denis Merigoux - - - 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 . *) - -exception Stop_instruction of Com.stop_kind - -let exit_on_rte = ref true - -let repl_debug = ref false - -module type S = sig - type custom_float - - type value = Number of custom_float | Undefined - - val format_value : Format.formatter -> value -> unit - - val format_value_prec : int -> int -> Format.formatter -> value -> unit - - type ctx_tmp_var = { mutable var : Com.Var.t; mutable value : value } - - type ctx_ref_var = { - mutable var : Com.Var.t; - mutable var_space : Com.variable_space; - mutable ref_var : Com.Var.t; - mutable org : int; - } - - type print_ctx = { mutable indent : int; mutable is_newline : bool } - - type ctx_var_space = { - input : value Array.t; - computed : value Array.t; - base : value Array.t; - } - - type ctx = { - ctx_prog : Mir.program; - mutable ctx_target : Mir.target; - mutable ctx_var_space : int; - ctx_var_spaces : ctx_var_space Array.t; - ctx_tmps : ctx_tmp_var Array.t; - mutable ctx_tmps_org : int; - ctx_ref : ctx_ref_var Array.t; - mutable ctx_ref_org : int; - ctx_tab_map : Com.Var.t Array.t; - ctx_pr_out : print_ctx; - ctx_pr_err : print_ctx; - mutable ctx_anos : (Com.Error.t * string option) list; - mutable ctx_nb_anos : int; - mutable ctx_nb_discos : int; - mutable ctx_nb_infos : int; - mutable ctx_nb_bloquantes : int; - mutable ctx_archived_anos : StrSet.t; - mutable ctx_finalized_anos : (Com.Error.t * string option) list; - mutable ctx_exported_anos : (Com.Error.t * string option) list; - mutable ctx_events : (value, Com.Var.t) Com.event_value Array.t Array.t list; - } - - val empty_ctx : Mir.program -> ctx - - val literal_to_value : Com.literal -> value - - val value_to_literal : value -> Com.literal - - val update_ctx_with_inputs : ctx -> Com.literal Com.Var.Map.t -> unit - - val update_ctx_with_events : - ctx -> (Com.literal, Com.Var.t) Com.event_value StrMap.t list -> unit - - type run_error = - | NanOrInf of string * Mir.expression Pos.marked - | StructuredError of - (string * (string option * Pos.t) list * (unit -> unit) option) - - exception RuntimeError of run_error * ctx - - val raise_runtime_as_structured : run_error -> 'a - - val compare_numbers : Com.comp_op -> custom_float -> custom_float -> bool - - val evaluate_expr : ctx -> Mir.expression Pos.marked -> value - - val evaluate_program : ctx -> unit -end - -module Make (N : Mir_number.NumberInterface) (RF : Mir_roundops.RoundOpsFunctor) = -struct - (* Careful : this behavior mimics the one imposed by the original Mlang - compiler... *) - - module R = RF (N) - - type custom_float = N.t - - let truncatef (x : N.t) : N.t = R.truncatef x - - let roundf (x : N.t) = R.roundf x - - type value = Number of N.t | Undefined - - let false_value () = Number (N.zero ()) - - let true_value () = Number (N.one ()) - - let format_value (fmt : Format.formatter) (x : value) = - match x with - | Undefined -> Com.format_literal fmt Com.Undefined - | Number x -> N.format_t fmt x - - let format_value_prec (mi : int) (ma : int) (fmt : Format.formatter) - (x : value) = - match x with - | Undefined -> Com.format_literal fmt Com.Undefined - | Number x -> N.format_prec_t mi ma fmt x - - type ctx_tmp_var = { mutable var : Com.Var.t; mutable value : value } - - type ctx_ref_var = { - mutable var : Com.Var.t; - mutable var_space : Com.variable_space; - mutable ref_var : Com.Var.t; - mutable org : int; - } - - type print_ctx = { mutable indent : int; mutable is_newline : bool } - - type ctx_var_space = { - input : value Array.t; - computed : value Array.t; - base : value Array.t; - } - - type ctx = { - ctx_prog : Mir.program; - mutable ctx_target : Mir.target; - mutable ctx_var_space : int; - ctx_var_spaces : ctx_var_space Array.t; - ctx_tmps : ctx_tmp_var Array.t; - mutable ctx_tmps_org : int; - ctx_ref : ctx_ref_var Array.t; - mutable ctx_ref_org : int; - ctx_tab_map : Com.Var.t Array.t; - ctx_pr_out : print_ctx; - ctx_pr_err : print_ctx; - mutable ctx_anos : (Com.Error.t * string option) list; - mutable ctx_nb_anos : int; - mutable ctx_nb_discos : int; - mutable ctx_nb_infos : int; - mutable ctx_nb_bloquantes : int; - mutable ctx_archived_anos : StrSet.t; - mutable ctx_finalized_anos : (Com.Error.t * string option) list; - mutable ctx_exported_anos : (Com.Error.t * string option) list; - mutable ctx_events : (value, Com.Var.t) Com.event_value Array.t Array.t list; - } - - type pctx = { - std : Com.print_std; - ctx : ctx; - std_fmt : Format.formatter; - ctx_pr : print_ctx; - } - - let empty_ctx (p : Mir.program) : ctx = - let dummy_var = Com.Var.new_ref ~name:(Pos.without "") in - let init_tmp_var _i = { var = dummy_var; value = Undefined } in - let init_ref _i = - { - var = dummy_var; - var_space = p.program_var_space_def; - ref_var = dummy_var; - org = -1; - } - in - let ctx_tab_map = - let init i = IntMap.find i p.program_stats.table_map in - Array.init (IntMap.cardinal p.program_stats.table_map) init - in - let ctx_var_spaces = - let init i = - let vsd = IntMap.find i p.program_var_spaces_idx in - let input = - if Com.CatVar.LocMap.mem Com.CatVar.LocInput vsd.vs_cats then - Array.make p.program_stats.sz_input Undefined - else Array.make 0 Undefined - in - let computed = - if Com.CatVar.LocMap.mem Com.CatVar.LocComputed vsd.vs_cats then - Array.make p.program_stats.sz_computed Undefined - else Array.make 0 Undefined - in - let base = - if Com.CatVar.LocMap.mem Com.CatVar.LocBase vsd.vs_cats then - Array.make p.program_stats.sz_base Undefined - else Array.make 0 Undefined - in - { input; computed; base } - in - Array.init (IntMap.cardinal p.program_var_spaces_idx) init - in - { - ctx_prog = p; - ctx_target = snd (StrMap.min_binding p.program_targets); - ctx_var_space = p.program_var_space_def.vs_id; - ctx_var_spaces; - ctx_tmps = Array.init p.program_stats.sz_all_tmps init_tmp_var; - ctx_tmps_org = 0; - ctx_ref = Array.init p.program_stats.nb_all_refs init_ref; - ctx_ref_org = 0; - ctx_tab_map; - ctx_pr_out = { indent = 0; is_newline = true }; - ctx_pr_err = { indent = 0; is_newline = true }; - ctx_anos = []; - ctx_nb_anos = 0; - ctx_nb_discos = 0; - ctx_nb_infos = 0; - ctx_nb_bloquantes = 0; - ctx_archived_anos = StrSet.empty; - ctx_finalized_anos = []; - ctx_exported_anos = []; - ctx_events = []; - } - - let literal_to_value (l : Com.literal) : value = - match l with - | Com.Undefined -> Undefined - | Com.Float f -> Number (N.of_float f) - - let value_to_literal (l : value) : Com.literal = - match l with - | Undefined -> Com.Undefined - | Number f -> Com.Float (N.to_float f) - - let update_ctx_with_inputs (ctx : ctx) (inputs : Com.literal Com.Var.Map.t) : - unit = - let value_inputs = - Com.Var.Map.mapi - (fun v l -> - match l with - | Com.Undefined -> Undefined - | Com.Float f -> Number (N.of_float_input v f)) - inputs - in - let default_space = - ctx.ctx_var_spaces.(ctx.ctx_prog.program_var_space_def.vs_id) - in - Com.Var.Map.iter - (fun (var : Com.Var.t) value -> - match Com.Var.cat_var_loc var with - | LocInput -> default_space.input.(Com.Var.loc_idx var) <- value - | LocComputed -> default_space.computed.(Com.Var.loc_idx var) <- value - | LocBase -> default_space.base.(Com.Var.loc_idx var) <- value) - value_inputs - - let update_ctx_with_events (ctx : ctx) - (events : (Com.literal, Com.Var.t) Com.event_value StrMap.t list) : unit = - let nbEvt = List.length events in - let ctx_event_tab = Array.make nbEvt [||] in - let fold idx (evt : (Com.literal, Com.Var.t) Com.event_value StrMap.t) = - let nbProgFields = StrMap.cardinal ctx.ctx_prog.program_event_fields in - let map = Array.make nbProgFields (Com.Numeric Undefined) in - for id = 0 to nbProgFields - 1 do - let fname = IntMap.find id ctx.ctx_prog.program_event_field_idxs in - let ef = StrMap.find fname ctx.ctx_prog.program_event_fields in - if ef.is_var then - map.(id) <- - Com.RefVar (snd (StrMap.min_binding ctx.ctx_prog.program_vars)) - done; - let iter' fname ev = - match StrMap.find_opt fname ctx.ctx_prog.program_event_fields with - | Some ef -> ( - match (ev, ef.is_var) with - | Com.Numeric Com.Undefined, false -> - map.(ef.index) <- Com.Numeric Undefined - | Com.Numeric (Com.Float f), false -> - map.(ef.index) <- Com.Numeric (Number (N.of_float f)) - | Com.RefVar v, true -> map.(ef.index) <- Com.RefVar v - | _ -> Errors.raise_error "wrong event field type") - | None -> Errors.raise_error "unknown event field" - in - StrMap.iter iter' evt; - ctx_event_tab.(idx) <- map; - idx + 1 - in - ignore (List.fold_left fold 0 events); - (* let max_field_length = - StrMap.fold - (fun s _ r -> max r (String.length s)) - ctx.ctx_prog.program_event_fields 0 - in - let pp_field fmt s = - let l = String.length s in - Format.fprintf fmt "%s%s" s (String.make (max_field_length - l + 1) ' ') - in - let pp_ev fmt = function - | Com.Numeric Undefined -> Pp.string fmt "indefini" - | Com.Numeric (Number v) -> N.format_t fmt v - | Com.RefVar v -> Pp.string fmt (Com.Var.name_str v) - in - for i = 0 to Array.length ctx_event_tab - 1 do - Format.eprintf "%d@." i; - let map = ctx_event_tab.(i) in - for j = 0 to Array.length map - 1 do - let s = IntMap.find j ctx.ctx_prog.program_event_field_idxs in - Format.eprintf " %a%a@." pp_field s pp_ev map.(j) - done - done;*) - ctx.ctx_events <- [ ctx_event_tab ] - - type run_error = - | NanOrInf of string * Mir.expression Pos.marked - | StructuredError of - (string * (string option * Pos.t) list * (unit -> unit) option) - - exception RuntimeError of run_error * ctx - - let raise_runtime_as_structured (e : run_error) = - match e with - | NanOrInf (v, e) -> - Errors.raise_spanned_error - (Format.asprintf "Expression evaluated to %s: %a" v - Format_mir.format_expression (Pos.unmark e)) - (Pos.get e) - | StructuredError (msg, pos, kont) -> - raise (Errors.StructuredError (msg, pos, kont)) - - let is_zero (l : value) : bool = - match l with Number z -> N.is_zero z | _ -> false - - let real_of_bool (b : bool) = if b then N.one () else N.zero () - - let bool_of_real (f : N.t) : bool = not N.(f =. zero ()) - - let compare_numbers op i1 i2 = - let epsilon = N.of_float !Config.comparison_error_margin in - let open Com in - match op with - | Gt -> N.(i1 >. i2 +. epsilon) - | Gte -> N.(i1 >. i2 -. epsilon) - | Lt -> N.(i1 +. epsilon <. i2) - | Lte -> N.(i1 -. epsilon <. i2) - | Eq -> N.(N.abs (i1 -. i2) <. epsilon) - | Neq -> N.(N.abs (i1 -. i2) >=. epsilon) - - let get_var_space (ctx : ctx) (m_sp_opt : Com.var_space) = - let i_sp = - match m_sp_opt with None -> ctx.ctx_var_space | Some (_, i_sp) -> i_sp - in - IntMap.find i_sp ctx.ctx_prog.program_var_spaces_idx - - let get_var (ctx : ctx) (m_sp_opt : Com.var_space) (var : Com.Var.t) : - Com.variable_space * Com.Var.t * int = - match var.scope with - | Com.Var.Tgv _ -> (get_var_space ctx m_sp_opt, var, 0) - | Com.Var.Temp _ -> (get_var_space ctx None, var, ctx.ctx_tmps_org) - | Com.Var.Ref -> - let rv = ctx.ctx_ref.(ctx.ctx_ref_org + Com.Var.loc_idx var) in - let vsd = - match m_sp_opt with - | None -> rv.var_space - | _ -> get_var_space ctx m_sp_opt - in - (vsd, rv.ref_var, rv.org) - - let get_var_tab (ctx : ctx) (var : Com.Var.t) (i : int) : Com.Var.t = - match Com.Var.get_table var with - | Some _ -> ctx.ctx_tab_map.(Com.Var.loc_tab_idx var + 1 + i) - | None -> assert false - - let get_var_value_org (ctx : ctx) (vsd : Com.variable_space) (var : Com.Var.t) - (vorg : int) : value = - let vi = Com.Var.loc_idx var in - match var.scope with - | Com.Var.Tgv _ -> - let var_space = ctx.ctx_var_spaces.(vsd.vs_id) in - let var_tab = - match Com.Var.cat_var_loc var with - | LocInput -> var_space.input - | LocComputed -> var_space.computed - | LocBase -> var_space.base - in - if Array.length var_tab > 0 then var_tab.(vi) else Undefined - | Com.Var.Temp _ -> ctx.ctx_tmps.(vorg + vi).value - | Com.Var.Ref -> assert false - - let get_var_value (ctx : ctx) (m_sp_opt : Com.var_space) (v : Com.Var.t) : - value = - let vsd, var, vorg = get_var ctx m_sp_opt v in - let var = if Com.Var.is_table var then get_var_tab ctx var 0 else var in - get_var_value_org ctx vsd var vorg - - let get_var_value_tab (ctx : ctx) (m_sp_opt : Com.var_space) (v : Com.Var.t) - (i : int) : value = - let vsd, var, vorg = get_var ctx m_sp_opt v in - if i < 0 then Number (N.zero ()) - else if Com.Var.size var <= i then Undefined - else if Com.Var.is_table var then - let var_i = get_var_tab ctx var i in - get_var_value_org ctx vsd var_i vorg - else get_var_value_org ctx vsd var vorg - - let set_var_ref (ctx : ctx) (var : Com.Var.t) (var_space : Com.variable_space) - (ref_var : Com.Var.t) (org : int) : unit = - match var.loc with - | LocRef (_, i) -> - ctx.ctx_ref.(ctx.ctx_ref_org + i).var <- var; - ctx.ctx_ref.(ctx.ctx_ref_org + i).var_space <- var_space; - ctx.ctx_ref.(ctx.ctx_ref_org + i).ref_var <- ref_var; - ctx.ctx_ref.(ctx.ctx_ref_org + i).org <- org - | _ -> assert false - - let mode_corr (ctx : ctx) = - match StrMap.find_opt "MODE_CORR" ctx.ctx_prog.program_vars with - | Some var -> ( - let vsd = ctx.ctx_prog.program_var_space_def in - let _, var, vorg = get_var ctx None var in - match get_var_value_org ctx vsd var vorg with - | Undefined -> false - | Number n -> compare_numbers Eq n (N.one ())) - | None -> false - - exception BlockingError - - let rec get_access_value ctx access = - match access with - | Com.VarAccess (m_sp_opt, v) -> get_var_value ctx m_sp_opt v - | Com.TabAccess ((m_sp_opt, v), m_idx) -> ( - match evaluate_expr ctx m_idx with - | Number z -> - let i = Int64.to_int @@ N.to_int z in - get_var_value_tab ctx m_sp_opt v i - | Undefined -> Undefined) - | Com.FieldAccess (m_sp_opt, e, _, j) -> ( - match evaluate_expr ctx e with - | Number z -> - let i = Int64.to_int @@ N.to_int z in - let events = List.hd ctx.ctx_events in - if 0 <= i && i < Array.length events then - match events.(i).(j) with - | Com.Numeric n -> n - | Com.RefVar v -> get_var_value ctx m_sp_opt v - else Undefined - | Undefined -> Undefined) - - and get_access_var ctx access = - match access with - | Com.VarAccess (m_sp_opt, v) -> - let vsd, v, vorg = get_var ctx m_sp_opt v in - Some (vsd, v, vorg) - | Com.TabAccess ((m_sp_opt, m_v), m_i) -> ( - match evaluate_expr ctx m_i with - | Number z -> - let vsd, v, vorg = get_var ctx m_sp_opt m_v in - let i = Int64.to_int @@ N.to_int z in - if 0 <= i && i < Com.Var.size v then - if Com.Var.is_table v then - let v_i = get_var_tab ctx v i in - Some (vsd, v_i, vorg) - else Some (vsd, v, vorg) - else None - | Undefined -> None) - | Com.FieldAccess (m_sp_opt, m_e, _, j) -> ( - match evaluate_expr ctx m_e with - | Number z -> - let i = Int64.to_int @@ N.to_int z in - let events = List.hd ctx.ctx_events in - if 0 <= i && i < Array.length events then - match events.(i).(j) with - | Com.RefVar v -> - let vsd, var, vorg = get_var ctx m_sp_opt v in - Some (vsd, var, vorg) - | Com.Numeric _ -> None - else None - | _ -> None) - - and set_var_value_org (ctx : ctx) (vsd : Com.variable_space) (var : Com.Var.t) - (vorg : int) (value : value) : unit = - let vi = Com.Var.loc_idx var in - match var.scope with - | Com.Var.Tgv _ -> - let var_space = ctx.ctx_var_spaces.(vsd.vs_id) in - let var_tab = - match Com.Var.cat_var_loc var with - | LocInput -> var_space.input - | LocComputed -> var_space.computed - | LocBase -> var_space.base - in - if Array.length var_tab > 0 then var_tab.(vi) <- value - | Com.Var.Temp _ -> ctx.ctx_tmps.(vorg + vi).value <- value - | Com.Var.Ref -> assert false - - and set_var_value (ctx : ctx) (m_sp_opt : Com.var_space) (var : Com.Var.t) - (value : value) : unit = - let vsd, v, vorg = get_var ctx m_sp_opt var in - if Com.Var.is_table v then - for i = 0 to Com.Var.size v - 1 do - let v_i = get_var_tab ctx v i in - set_var_value_org ctx vsd v_i vorg value - done - else set_var_value_org ctx vsd v vorg value - - and set_var_value_tab (ctx : ctx) (m_sp_opt : Com.var_space) (v : Com.Var.t) - (i : int) (value : value) : unit = - let vsd, var, vorg = get_var ctx m_sp_opt v in - if 0 <= i && i < Com.Var.size var then - if Com.Var.is_table var then - let var_i = get_var_tab ctx var i in - set_var_value_org ctx vsd var_i vorg value - else set_var_value_org ctx vsd var vorg value - - and evaluate_switch_expr (ctx : ctx) s_e = - match s_e with - | Com.SEValue e -> ( - match evaluate_expr ctx e with - | Undefined -> `Undefined - | Number n -> `Value n) - | SESameVariable v -> `Var v - - and set_access ctx access value = - match access with - | Com.VarAccess (m_sp_opt, v) -> set_var_value ctx m_sp_opt v value - | Com.TabAccess ((m_sp_opt, v), m_idx) -> ( - match evaluate_expr ctx m_idx with - | Number z -> - let i = Int64.to_int @@ N.to_int z in - set_var_value_tab ctx m_sp_opt v i value - | Undefined -> ()) - | Com.FieldAccess (m_sp_opt, e, _, j) -> ( - match evaluate_expr ctx e with - | Number z -> ( - let i = Int64.to_int @@ N.to_int z in - let events = List.hd ctx.ctx_events in - if 0 <= i && i < Array.length events then - match events.(i).(j) with - | Com.Numeric _ -> events.(i).(j) <- Com.Numeric value - | Com.RefVar v -> set_var_value ctx m_sp_opt v value) - | Undefined -> ()) - - (* print aux *) - - and pr_ctx std ctx = - match std with - | Com.StdOut -> - { std; ctx; std_fmt = Format.std_formatter; ctx_pr = ctx.ctx_pr_out } - | Com.StdErr -> - { std; ctx; std_fmt = Format.err_formatter; ctx_pr = ctx.ctx_pr_err } - - and pr_flush (pctx : pctx) = - match pctx.std with - | Com.StdOut -> () - | Com.StdErr -> Format.pp_print_flush pctx.std_fmt () - - and pr_out_indent (pctx : pctx) = - if pctx.ctx_pr.is_newline then ( - for _i = 1 to pctx.ctx_pr.indent do - Format.fprintf pctx.std_fmt " " - done; - pctx.ctx_pr.is_newline <- false) - - and pr_raw (pctx : pctx) s = - let len = String.length s in - let rec aux = function - | n when n >= len -> () - | n -> ( - match s.[n] with - | '\n' -> - Format.fprintf pctx.std_fmt "\n"; - pr_flush pctx; - pctx.ctx_pr.is_newline <- true; - aux (n + 1) - | c -> - pr_out_indent pctx; - Format.fprintf pctx.std_fmt "%c" c; - aux (n + 1)) - in - aux 0 - - and pr_set_indent (pctx : pctx) diff = - pctx.ctx_pr.indent <- max 0 (pctx.ctx_pr.indent + diff) - - and pr_value (pctx : pctx) mi ma value = - pr_raw pctx (Pp.spr "%a" (format_value_prec mi ma) value) - - and pr_info (pctx : pctx) info (vsd : Com.variable_space) var = - if not vsd.vs_by_default then ( - pr_raw pctx (Pos.unmark vsd.vs_name); - pr_raw pctx "."); - let _, v, _ = get_var pctx.ctx None var in - match info with - | Com.Name -> pr_raw pctx (Com.Var.name_str v) - | Com.Alias -> pr_raw pctx (Com.Var.alias_str v) - - and pr_string (pctx : pctx) s = - pr_raw pctx s; - pr_flush pctx - - and pr_access (pctx : pctx) info acc = - match get_access_var pctx.ctx acc with - | Some (vsd, var, _) -> - pr_info pctx info vsd var; - pr_flush pctx - | None -> () - - and pr_indent (pctx : pctx) e = - match evaluate_expr pctx.ctx e with - | Undefined -> () - | Number x -> - let diff = Int64.to_int @@ N.to_int @@ roundf x in - pr_set_indent pctx diff - - and pr_expr (pctx : pctx) mi ma e = - pr_value pctx mi ma (evaluate_expr pctx.ctx e); - pr_flush pctx - - (* interpret *) - - and evaluate_expr (ctx : ctx) (e : Mir.expression Pos.marked) : value = - let comparison op new_e1 new_e2 = - match (op, new_e1, new_e2) with - | Com.(Gt | Gte | Lt | Lte | Eq | Neq), _, Undefined - | Com.(Gt | Gte | Lt | Lte | Eq | Neq), Undefined, _ -> - Undefined - | op, Number i1, Number i2 -> - Number (real_of_bool @@ compare_numbers op i1 i2) - in - let unop op new_e1 = - match (op, new_e1) with - | Com.Not, Number b1 -> Number (real_of_bool (not (bool_of_real b1))) - | Com.Minus, Number f1 -> Number N.(zero () -. f1) - | Com.(Not | Minus), Undefined -> Undefined - in - let binop op new_e1 new_e2 = - let open Com in - match (op, new_e1, new_e2) with - | Add, Number i1, Number i2 -> Number N.(i1 +. i2) - | Add, Number i1, Undefined -> Number N.(i1 +. zero ()) - | Add, Undefined, Number i2 -> Number N.(zero () +. i2) - | Add, Undefined, Undefined -> Undefined - | Sub, Number i1, Number i2 -> Number N.(i1 -. i2) - | Sub, Number i1, Undefined -> Number N.(i1 -. zero ()) - | Sub, Undefined, Number i2 -> Number N.(zero () -. i2) - | Sub, Undefined, Undefined -> Undefined - | Mul, _, Undefined | Mul, Undefined, _ -> Undefined - | Mul, Number i1, Number i2 -> Number N.(i1 *. i2) - | Div, Undefined, _ | Div, _, Undefined -> Undefined (* yes... *) - | Div, _, l2 when is_zero l2 -> Number (N.zero ()) - | Div, Number i1, Number i2 -> Number N.(i1 /. i2) - | Mod, Undefined, _ | Mod, _, Undefined -> Undefined (* yes... *) - | Mod, _, l2 when is_zero l2 -> Number (N.zero ()) - | Mod, Number i1, Number i2 -> Number N.(i1 %. i2) - | And, Undefined, _ | And, _, Undefined -> Undefined - | Or, Undefined, Undefined -> Undefined - | Or, Undefined, Number i | Or, Number i, Undefined -> Number i - | And, Number i1, Number i2 -> - Number (real_of_bool (bool_of_real i1 && bool_of_real i2)) - | Or, Number i1, Number i2 -> - Number (real_of_bool (bool_of_real i1 || bool_of_real i2)) - in - let out = - try - match Pos.unmark e with - | Com.TestInSet (positive, e0, values) -> - let value0 = evaluate_expr ctx e0 in - let or_chain = - List.fold_left - (fun or_chain set_value -> - let equal_test = - match set_value with - | Com.VarValue (Pos.Mark (access, _)) -> - let value = get_access_value ctx access in - comparison Com.Eq value0 value - | Com.FloatValue i -> - let value_i = Number (N.of_float @@ Pos.unmark i) in - comparison Com.Eq value0 value_i - | Com.IntervalValue (bn, en) -> - let value_bn = - Number (N.of_float @@ float_of_int @@ Pos.unmark bn) - in - let value_en = - Number (N.of_float @@ float_of_int @@ Pos.unmark en) - in - binop Com.And - (comparison Com.Gte value0 value_bn) - (comparison Com.Lte value0 value_en) - in - binop Com.Or or_chain equal_test) - Undefined values - in - if positive then or_chain else unop Com.Not or_chain - | Comparison (op, e1, e2) -> - let value1 = evaluate_expr ctx e1 in - let value2 = evaluate_expr ctx e2 in - comparison (Pos.unmark op) value1 value2 - | Binop (op, e1, e2) -> - let value1 = evaluate_expr ctx e1 in - let value2 = evaluate_expr ctx e2 in - binop (Pos.unmark op) value1 value2 - | Unop (op, e1) -> unop op @@ evaluate_expr ctx e1 - | Conditional (e1, e2, e3_opt) -> ( - match evaluate_expr ctx e1 with - | Number z when N.(z =. zero ()) -> ( - match e3_opt with - | None -> Undefined - | Some e3 -> evaluate_expr ctx e3) - | Number _ -> evaluate_expr ctx e2 - | Undefined -> Undefined) - | Literal Undefined -> Undefined - | Literal (Float f) -> Number (N.of_float f) - | Var access -> get_access_value ctx access - | FuncCall (Pos.Mark (ArrFunc, _), [ arg ]) -> ( - match evaluate_expr ctx arg with - | Number x -> Number (roundf x) - | Undefined -> Undefined (*nope:Float 0.*)) - | FuncCall (Pos.Mark (InfFunc, _), [ arg ]) -> ( - match evaluate_expr ctx arg with - | Number x -> Number (truncatef x) - | Undefined -> Undefined (*Float 0.*)) - | FuncCall (Pos.Mark (PresentFunc, _), [ arg ]) -> ( - match evaluate_expr ctx arg with - | Undefined -> false_value () - | _ -> true_value ()) - | FuncCall (Pos.Mark (Supzero, _), [ arg ]) -> ( - match evaluate_expr ctx arg with - | Undefined -> Undefined - | Number f as n -> - if compare_numbers Com.Lte f (N.zero ()) then Undefined else n) - | FuncCall (Pos.Mark (AbsFunc, _), [ arg ]) -> ( - match evaluate_expr ctx arg with - | Undefined -> Undefined - | Number f -> Number (N.abs f)) - | FuncCall (Pos.Mark (MinFunc, _), [ arg1; arg2 ]) -> ( - match (evaluate_expr ctx arg1, evaluate_expr ctx arg2) with - | Undefined, Undefined -> Undefined - | Undefined, Number f | Number f, Undefined -> - Number (N.min (N.zero ()) f) - | Number fl, Number fr -> Number (N.min fl fr)) - | FuncCall (Pos.Mark (MaxFunc, _), [ arg1; arg2 ]) -> ( - match (evaluate_expr ctx arg1, evaluate_expr ctx arg2) with - | Undefined, Undefined -> Undefined - | Undefined, Number f | Number f, Undefined -> - Number (N.max (N.zero ()) f) - | Number fl, Number fr -> Number (N.max fl fr)) - | FuncCall (Pos.Mark (Multimax, _), [ arg1; arg2 ]) -> ( - match evaluate_expr ctx arg1 with - | Undefined -> Undefined - | Number f -> ( - let nb = Int64.to_int @@ N.to_int @@ roundf f in - let var_opt = - match Pos.unmark arg2 with - | Var access -> get_access_var ctx access - | _ -> None - in - match var_opt with - | None -> Undefined - | Some (vsd, var, vorg) -> - if Com.Var.is_table var then - let rec loop res i = - if i >= Com.Var.size var || i >= nb then res - else - let var_i = get_var_tab ctx var i in - let val_i = get_var_value_org ctx vsd var_i vorg in - let res = - match (res, val_i) with - | Undefined, _ -> val_i - | Number _, Undefined -> res - | Number nr, Number ni -> - if N.(nr <. ni) then val_i else res - in - loop res (i + 1) - in - loop Undefined 0 - else if nb >= 1 then get_var_value_org ctx vsd var vorg - else Undefined)) - | FuncCall (Pos.Mark (NbEvents, _), _) -> - let card = Array.length (List.hd ctx.ctx_events) in - Number (N.of_int @@ Int64.of_int @@ card) - | FuncCall (Pos.Mark (Func fn, _), args) -> - let fd = StrMap.find fn ctx.ctx_prog.program_functions in - evaluate_function ctx fd args - | FuncCall (_, _) -> assert false - | Attribut (m_acc, a) -> ( - match get_access_var ctx (Pos.unmark m_acc) with - | Some (_, v, _) -> ( - match StrMap.find_opt (Pos.unmark a) (Com.Var.attrs v) with - | Some l -> Number (N.of_float (float (Pos.unmark l))) - | None -> Undefined) - | None -> Undefined) - | Size m_acc -> ( - match get_access_var ctx (Pos.unmark m_acc) with - | Some (_, v, _) -> Number (N.of_float @@ float @@ Com.Var.size v) - | None -> Undefined) - | Type (m_acc, m_typ) -> ( - match get_access_var ctx (Pos.unmark m_acc) with - | Some (_, v, _) -> - if Com.Var.is_tgv v && Com.Var.typ v = Some (Pos.unmark m_typ) - then Number (N.one ()) - else Number (N.zero ()) - | None -> Undefined) - | SameVariable (m_acc0, m_acc1) -> - if same_variable ctx m_acc0 m_acc1 then Number (N.one ()) - else Number (N.zero ()) - | InDomain (m_acc, cvm) -> ( - match get_access_var ctx (Pos.unmark m_acc) with - | Some (_, v, _) -> - if Com.Var.is_tgv v && Com.CatVar.Map.mem (Com.Var.cat v) cvm - then Number (N.one ()) - else Number (N.zero ()) - | None -> Number (N.zero ())) - | NbAnomalies -> Number (N.of_float (float ctx.ctx_nb_anos)) - | NbDiscordances -> Number (N.of_float (float ctx.ctx_nb_discos)) - | NbInformatives -> Number (N.of_float (float ctx.ctx_nb_infos)) - | NbBloquantes -> Number (N.of_float (float ctx.ctx_nb_bloquantes)) - | NbCategory _ | FuncCallLoop _ | Loop _ -> assert false - with - | RuntimeError (e, ctx) -> - if !exit_on_rte then raise_runtime_as_structured e - else raise (RuntimeError (e, ctx)) - | Errors.StructuredError (msg, pos, kont) -> - if !exit_on_rte then - raise - (Errors.StructuredError - ( msg, - pos @ [ (Some "Expression raising the error:", Pos.get e) ], - kont )) - else raise (RuntimeError (StructuredError (msg, pos, kont), ctx)) - in - if match out with Undefined -> false | Number out -> N.is_nan_or_inf out - then - let e = - NanOrInf - ( (match out with - | Undefined -> assert false - | Number out -> Format.asprintf "%a" N.format_t out), - e ) - in - if !exit_on_rte then raise_runtime_as_structured e - else raise (RuntimeError (e, ctx)) - else out - - and same_variable ctx m_acc m_acc' : bool = - let v0_opt = get_access_var ctx (Pos.unmark m_acc) in - let v1_opt = get_access_var ctx (Pos.unmark m_acc') in - match (v0_opt, v1_opt) with - | Some (_, v0, _), Some (_, v1, _) -> - Com.Var.name_str v0 = Com.Var.name_str v1 - | _, _ -> false - - and evaluate_stmt (canBlock : bool) (ctx : ctx) (stmt : Mir.m_instruction) : - unit = - match Pos.unmark stmt with - | Com.Affectation (Pos.Mark (SingleFormula (VarDecl (m_acc, vexpr)), _)) -> - set_access ctx (Pos.unmark m_acc) @@ evaluate_expr ctx vexpr - | Com.Affectation - (Pos.Mark (SingleFormula (EventFieldRef (idx, _, j, var)), _)) -> ( - match evaluate_expr ctx idx with - | Number z when N.(z >=. zero ()) -> ( - let i = Int64.to_int @@ N.to_int z in - let events = List.hd ctx.ctx_events in - if 0 <= i && i < Array.length events then - match events.(i).(j) with - | Com.RefVar _ -> - let _, v, _ = get_var ctx None var in - if Com.Var.is_tgv v && not (Com.Var.is_table v) then - events.(i).(j) <- Com.RefVar v - | Com.Numeric _ -> ()) - | _ -> ()) - | Com.Affectation (Pos.Mark (Com.MultipleFormulaes _, _)) -> assert false - | Com.IfThenElse (b, t, f) -> ( - match evaluate_expr ctx b with - | Number z when N.(z =. zero ()) -> evaluate_stmts canBlock ctx f - | Number _ -> evaluate_stmts canBlock ctx t - | Undefined -> ()) - | Com.Switch (c, l) -> ( - let exception INTERNAL_STOP_SWITCH in - let then_ () = raise INTERNAL_STOP_SWITCH in - let v = evaluate_switch_expr ctx c in - let default = ref None in - try - List.iter - (fun (cases, stmts) -> - List.iter - (fun case -> - match (case, v) with - | Com.CDefault, _ -> - (* Trigged only if all other cases fail *) - default := Some stmts - | CValue Undefined, `Undefined -> - evaluate_stmts ~then_ canBlock ctx stmts - | CValue _, `Undefined | CValue Undefined, _ -> () - | CValue (Float f), `Value v -> - if N.of_float f = v then - evaluate_stmts ~then_ canBlock ctx stmts - | CValue _, `Var _ -> - failwith "Cannot match value with variable" - | CVar m_acc, `Var v -> - if same_variable ctx m_acc v then - evaluate_stmts ~then_ canBlock ctx stmts - | CVar _, (`Value _ | `Undefined) -> - failwith "Cannot match variable with value") - cases) - l - with INTERNAL_STOP_SWITCH -> ()) - | Com.WhenDoElse (wdl, ed) -> - let rec aux = function - | (expr, dl, _) :: l -> ( - match evaluate_expr ctx expr with - | Number z when N.(z =. zero ()) -> - evaluate_stmts canBlock ctx (Pos.unmark ed) - | Number _ -> - evaluate_stmts canBlock ctx dl; - aux l - | Undefined -> aux l) - | [] -> () - in - aux wdl - | Com.VerifBlock stmts -> evaluate_stmts true ctx stmts - | Com.ComputeTarget (Pos.Mark (tn, _), args, m_sp_opt) -> - let tf = StrMap.find tn ctx.ctx_prog.program_targets in - let vsd = get_var_space ctx m_sp_opt in - evaluate_target canBlock ctx tf args vsd - | Com.Print (std, args) -> - let pctx = pr_ctx std ctx in - List.iter - (fun (arg : Com.Var.t Com.print_arg Pos.marked) -> - match Pos.unmark arg with - | PrintString s -> pr_string pctx s - | PrintAccess (info, m_a) -> pr_access pctx info (Pos.unmark m_a) - | PrintIndent e -> pr_indent pctx e - | PrintExpr (e, mi, ma) -> pr_expr pctx mi ma e) - args; - pr_flush pctx - | Com.Iterate ((var : Com.Var.t), al, var_params, stmts) -> ( - try - List.iter - (fun m_a -> - match get_access_var ctx @@ Pos.unmark m_a with - | Some (vsd, v, vorg) -> - set_var_ref ctx var vsd v vorg; - evaluate_stmts canBlock ctx stmts - | None -> ()) - al; - List.iter - (fun (vcs, expr, m_sp_opt) -> - let eval vc _ = - StrMap.iter - (fun _ v -> - if - Com.CatVar.compare (Com.Var.cat v) vc = 0 - && not (Com.Var.is_table v) - then ( - let vsd, v, org = get_var ctx m_sp_opt v in - set_var_ref ctx var vsd v org; - match evaluate_expr ctx expr with - | Number z when N.(z =. one ()) -> - evaluate_stmts canBlock ctx stmts - | _ -> ())) - ctx.ctx_prog.program_vars - in - Com.CatVar.Map.iter eval vcs) - var_params - with - | Stop_instruction (SKId None) -> () - | Stop_instruction (SKId (Some scope)) as exn -> - if scope = Pos.unmark var.name then () else raise exn) - | Com.Iterate_values ((var : Com.Var.t), var_intervals, stmts) -> ( - try - List.iter - (fun (e0, e1, step) -> - let val0 = evaluate_expr ctx e0 in - let val1 = evaluate_expr ctx e1 in - let valStep = evaluate_expr ctx step in - match (val0, val1, valStep) with - | Number z0, Number z1, Number zStep when not N.(is_zero zStep) -> - let cmp = N.(if zStep > zero () then ( <=. ) else ( >=. )) in - let rec loop i = - if cmp i z1 then ( - let vsd, var, vorg = get_var ctx None var in - set_var_value_org ctx vsd var vorg (Number i); - evaluate_stmts canBlock ctx stmts; - loop N.(i +. zStep)) - in - loop z0 - | _, _, _ -> ()) - var_intervals - with - | Stop_instruction (SKId None) -> () - | Stop_instruction (SKId (Some scope)) as exn -> - if scope = Pos.unmark var.name then () else raise exn) - | Com.Stop scope -> raise (Stop_instruction scope) - | Com.Restore (al, var_params, evts, evtfs, stmts) -> - let backup backup_vars vsd var vorg = - if Com.Var.is_table var then - let sz = Com.Var.size var in - let rec loop backup_vars i = - if i >= sz then backup_vars - else - let v_i = get_var_tab ctx var i in - let value = get_var_value_org ctx vsd v_i vorg in - loop ((vsd, v_i, vorg, value) :: backup_vars) (i + 1) - in - loop backup_vars 0 - else - let value = get_var_value_org ctx vsd var vorg in - (vsd, var, vorg, value) :: backup_vars - in - let backup_vars = - List.fold_left - (fun backup_vars m_acc -> - match get_access_var ctx (Pos.unmark m_acc) with - | Some (vsd, var, vorg) -> backup backup_vars vsd var vorg - | None -> backup_vars) - [] al - in - let backup_vars = - List.fold_left - (fun backup_vars ((var : Com.Var.t), vcs, expr, m_sp_opt) -> - Com.CatVar.Map.fold - (fun vc _ backup_vars -> - StrMap.fold - (fun _ v backup_vars -> - if Com.CatVar.compare (Com.Var.cat v) vc = 0 then ( - let vsd, v', vorg = get_var ctx m_sp_opt v in - set_var_ref ctx var vsd v' vorg; - match evaluate_expr ctx expr with - | Number z when N.(z =. one ()) -> - backup backup_vars vsd v' vorg - | _ -> backup_vars) - else backup_vars) - ctx.ctx_prog.program_vars backup_vars) - vcs backup_vars) - backup_vars var_params - in - let backup_evts = - List.fold_left - (fun backup_evts expr -> - match evaluate_expr ctx expr with - | Number z -> - let i = Int64.to_int @@ N.to_int z in - let events0 = List.hd ctx.ctx_events in - if 0 <= i && i < Array.length events0 then ( - let evt = events0.(i) in - events0.(i) <- Array.copy evt; - (i, evt) :: backup_evts) - else backup_evts - | _ -> backup_evts) - [] evts - in - let backup_evts = - List.fold_left - (fun backup_evts ((var : Com.Var.t), expr) -> - let events0 = List.hd ctx.ctx_events in - let rec aux backup_evts i = - if i < Array.length events0 then ( - let vi = N.of_int @@ Int64.of_int i in - set_var_value ctx None var (Number vi); - match evaluate_expr ctx expr with - | Number z when N.(z =. one ()) -> - let evt = events0.(i) in - events0.(i) <- Array.copy evt; - aux ((i, evt) :: backup_evts) (i + 1) - | _ -> aux backup_evts (i + 1)) - else backup_evts - in - aux backup_evts 0) - backup_evts evtfs - in - let then_ () = - List.iter - (fun (vsd, v, vorg, value) -> - set_var_value_org ctx vsd v vorg value) - backup_vars; - let events0 = List.hd ctx.ctx_events in - List.iter (fun (i, evt) -> events0.(i) <- evt) backup_evts - in - evaluate_stmts ~then_ canBlock ctx stmts - | Com.ArrangeEvents (sort, filter, add, stmts) -> - let event_list, nbAdd = - match add with - | Some expr -> ( - match evaluate_expr ctx expr with - | Number z when N.(z >. zero ()) -> - let nb = Int64.to_int @@ N.to_int z in - if nb > 0 then - let nbProgFields = - IntMap.cardinal ctx.ctx_prog.program_event_field_idxs - in - let defEvt = - let init id = - let fname = - IntMap.find id ctx.ctx_prog.program_event_field_idxs - in - let ef = - StrMap.find fname ctx.ctx_prog.program_event_fields - in - match ef.is_var with - | true -> - let defVar = - snd - @@ StrMap.min_binding ctx.ctx_prog.program_vars - in - Com.RefVar defVar - | false -> Com.Numeric Undefined - in - Array.init nbProgFields init - in - let init = function - | 0 -> defEvt - | _ -> Array.copy defEvt - in - (List.init nb init, nb) - else ([], 0) - | _ -> ([], 0)) - | None -> ([], 0) - in - let events = - match filter with - | Some (var, expr) -> - let events0 = List.hd ctx.ctx_events in - let rec aux res i = - if i >= Array.length events0 then Array.of_list (List.rev res) - else - let vi = Number (N.of_int @@ Int64.of_int i) in - set_var_value ctx None var vi; - let res' = - match evaluate_expr ctx expr with - | Number z when N.(z =. one ()) -> events0.(i) :: res - | _ -> res - in - aux res' (i + 1) - in - aux event_list 0 - | None -> - let events0 = List.hd ctx.ctx_events in - let rec aux res i = - if i >= Array.length events0 then Array.of_list (List.rev res) - else aux (events0.(i) :: res) (i + 1) - in - aux event_list 0 - in - ctx.ctx_events <- events :: ctx.ctx_events; - (match sort with - | Some (var0, var1, expr) -> - let sort_fun i _ j _ = - let vi = Number (N.of_int @@ Int64.of_int i) in - set_var_value ctx None var0 vi; - let vj = Number (N.of_int @@ Int64.of_int j) in - set_var_value ctx None var1 vj; - match evaluate_expr ctx expr with - | Number z when N.(z =. zero ()) -> false - | Number _ -> true - | Undefined -> false - in - Sorting.mergeSort sort_fun nbAdd (Array.length events) events - | None -> ()); - let then_ () = ctx.ctx_events <- List.tl ctx.ctx_events in - evaluate_stmts ~then_ canBlock ctx stmts - | Com.RaiseError (m_err, var_opt) -> - let err = Pos.unmark m_err in - (match err.typ with - | Com.Error.Anomaly -> ctx.ctx_nb_anos <- ctx.ctx_nb_anos + 1 - | Com.Error.Discordance -> ctx.ctx_nb_discos <- ctx.ctx_nb_discos + 1 - | Com.Error.Information -> ctx.ctx_nb_infos <- ctx.ctx_nb_infos + 1); - let is_blocking = - err.typ = Com.Error.Anomaly && Pos.unmark err.is_isf = "N" - in - ctx.ctx_nb_bloquantes <- - (ctx.ctx_nb_bloquantes + if is_blocking then 1 else 0); - let v_opt = Option.map Pos.unmark var_opt in - ctx.ctx_anos <- ctx.ctx_anos @ [ (err, v_opt) ]; - if is_blocking && ctx.ctx_nb_bloquantes >= 4 && canBlock then - raise BlockingError - | Com.CleanErrors -> - ctx.ctx_anos <- []; - ctx.ctx_nb_anos <- 0; - ctx.ctx_nb_discos <- 0; - ctx.ctx_nb_infos <- 0; - ctx.ctx_nb_bloquantes <- 0 - | Com.CleanFinalizedErrors -> ctx.ctx_finalized_anos <- [] - | Com.FinalizeErrors -> - let mem (ano : Com.Error.t) anos = - List.fold_left - (fun res ((a : Com.Error.t), _) -> - res || Pos.unmark a.name = Pos.unmark ano.name) - false anos - in - if mode_corr ctx then - let rec merge_anos () = - match ctx.ctx_anos with - | [] -> () - | ((ano : Com.Error.t), arg) :: discos -> - let cont = - if not (mem ano ctx.ctx_finalized_anos) then ( - ctx.ctx_finalized_anos <- - ctx.ctx_finalized_anos @ [ (ano, arg) ]; - ano.typ <> Com.Error.Anomaly) - else true - in - ctx.ctx_anos <- discos; - if cont then merge_anos () - in - merge_anos () - else ( - ctx.ctx_finalized_anos <- []; - let rec merge_anos () = - match ctx.ctx_anos with - | [] -> ctx.ctx_finalized_anos <- List.rev ctx.ctx_finalized_anos - | ((ano : Com.Error.t), arg) :: discos -> - if not (StrSet.mem (Pos.unmark ano.name) ctx.ctx_archived_anos) - then ( - ctx.ctx_archived_anos <- - StrSet.add (Pos.unmark ano.name) ctx.ctx_archived_anos; - ctx.ctx_finalized_anos <- (ano, arg) :: ctx.ctx_finalized_anos); - ctx.ctx_anos <- discos; - merge_anos () - in - merge_anos ()) - | Com.ExportErrors -> - if mode_corr ctx then - let rec merge_anos () = - match ctx.ctx_finalized_anos with - | [] -> () - | ((ano : Com.Error.t), arg) :: fins -> - if not (StrSet.mem (Pos.unmark ano.name) ctx.ctx_archived_anos) - then ( - ctx.ctx_archived_anos <- - StrSet.add (Pos.unmark ano.name) ctx.ctx_archived_anos; - ctx.ctx_exported_anos <- - ctx.ctx_exported_anos @ [ (ano, arg) ]); - ctx.ctx_finalized_anos <- fins; - merge_anos () - in - merge_anos () - else ( - ctx.ctx_exported_anos <- - ctx.ctx_exported_anos @ ctx.ctx_finalized_anos; - ctx.ctx_finalized_anos <- []) - | Com.ComputeDomain _ | Com.ComputeChaining _ | Com.ComputeVerifs _ -> - assert false - - and evaluate_stmts ?(then_ = ignore) canBlock (ctx : ctx) - (stmts : Mir.m_instruction list) : unit = - let () = - try List.iter (evaluate_stmt canBlock ctx) stmts with - | BlockingError as b_err -> if canBlock then raise b_err - | Stop_instruction _ as exn -> - then_ (); - raise exn - in - then_ () - - and evaluate_function (ctx : ctx) (target : Mir.target) - (args : Mir.m_expression list) : value = - let rec set_args n vl el = - match (vl, el) with - | [], [] -> () - | v :: vl', e :: el' -> - let i = ctx.ctx_tmps_org + n + 1 in - let e_val = evaluate_expr ctx e in - ctx.ctx_tmps.(i).var <- v; - ctx.ctx_tmps.(i).value <- e_val; - set_args (n + 1) vl' el' - | _ -> assert false - in - set_args 0 target.target_args args; - ctx.ctx_tmps.(ctx.ctx_tmps_org).var <- Option.get target.target_result; - ctx.ctx_tmps.(ctx.ctx_tmps_org).value <- Undefined; - evaluate_target_aux ~is_fun:true false ctx target; - ctx.ctx_tmps.(ctx.ctx_tmps_org).value - - and evaluate_target (canBlock : bool) (ctx : ctx) (target : Mir.target) - (args : Mir.m_access list) (vsd : Com.variable_space) : unit = - let rec set_args n vl al = - match (vl, al) with - | v :: vl', m_a :: al' -> ( - ctx.ctx_ref.(ctx.ctx_ref_org + n).var <- v; - match get_access_var ctx (Pos.unmark m_a) with - | Some (var_space, ref_var, org) -> - ctx.ctx_ref.(ctx.ctx_ref_org + n).var_space <- var_space; - ctx.ctx_ref.(ctx.ctx_ref_org + n).ref_var <- ref_var; - ctx.ctx_ref.(ctx.ctx_ref_org + n).org <- org; - set_args (n + 1) vl' al' - | None -> ()) - | [], [] -> - let vs_id_sav = ctx.ctx_var_space in - ctx.ctx_var_space <- vsd.vs_id; - evaluate_target_aux ~is_fun:false canBlock ctx target; - ctx.ctx_var_space <- vs_id_sav - | _ -> assert false - in - set_args 0 target.target_args args - - and evaluate_target_aux ~(is_fun : bool) (canBlock : bool) (ctx : ctx) - (target : Mir.target) : unit = - let sav_target = ctx.ctx_target in - ctx.ctx_target <- target; - ctx.ctx_tmps_org <- ctx.ctx_tmps_org + target.target_sz_tmps; - StrMap.iter - (fun _ v -> - let i = ctx.ctx_tmps_org + Com.Var.loc_idx v in - ctx.ctx_tmps.(i).var <- v; - ctx.ctx_tmps.(i).value <- Undefined) - target.target_tmp_vars; - ctx.ctx_ref_org <- ctx.ctx_ref_org + target.target_nb_refs; - let then_ () = - ctx.ctx_ref_org <- ctx.ctx_ref_org - target.target_nb_refs; - ctx.ctx_tmps_org <- ctx.ctx_tmps_org - target.target_sz_tmps - in - let () = - try evaluate_stmts ~then_ canBlock ctx target.target_prog with - | Stop_instruction SKTarget when not is_fun -> () - | Stop_instruction SKFun when is_fun -> () - in - ctx.ctx_target <- sav_target - - let evaluate_program (ctx : ctx) : unit = - try - let main_target = - match - StrMap.find_opt ctx.ctx_prog.program_main_target - ctx.ctx_prog.program_targets - with - | Some t -> t - | None -> - Errors.raise_error "Unable to find main function of Bir program" - in - let vsd = ctx.ctx_prog.program_var_space_def in - ctx.ctx_target <- main_target; - evaluate_target false ctx main_target [] vsd; - evaluate_stmt false ctx (Pos.without Com.ExportErrors) - with - | RuntimeError (e, ctx) -> - if !exit_on_rte then raise_runtime_as_structured e - else raise (RuntimeError (e, ctx)) - | Stop_instruction SKApplication -> - (* The only stop never caught by anything else *) () - | Stop_instruction SKTarget -> (* May not be caught by anything else *) () -end - -module BigIntPrecision = struct - let scaling_factor_bits = ref 64 -end - -module MainframeLongSize = struct - let max_long = ref Int64.max_int -end - -module FloatDefInterp = - Make (Mir_number.RegularFloatNumber) (Mir_roundops.DefaultRoundOps) -module FloatMultInterp = - Make (Mir_number.RegularFloatNumber) (Mir_roundops.MultiRoundOps) -module FloatMfInterp = - Make - (Mir_number.RegularFloatNumber) - (Mir_roundops.MainframeRoundOps (MainframeLongSize)) -module MPFRDefInterp = - Make (Mir_number.MPFRNumber) (Mir_roundops.DefaultRoundOps) -module MPFRMultInterp = - Make (Mir_number.MPFRNumber) (Mir_roundops.MultiRoundOps) -module MPFRMfInterp = - Make - (Mir_number.MPFRNumber) - (Mir_roundops.MainframeRoundOps (MainframeLongSize)) -module BigIntDefInterp = - Make - (Mir_number.BigIntFixedPointNumber - (BigIntPrecision)) - (Mir_roundops.DefaultRoundOps) -module BigIntMultInterp = - Make - (Mir_number.BigIntFixedPointNumber - (BigIntPrecision)) - (Mir_roundops.MultiRoundOps) -module BigIntMfInterp = - Make - (Mir_number.BigIntFixedPointNumber - (BigIntPrecision)) - (Mir_roundops.MainframeRoundOps (MainframeLongSize)) -module IntvDefInterp = - Make (Mir_number.IntervalNumber) (Mir_roundops.DefaultRoundOps) -module IntvMultInterp = - Make (Mir_number.IntervalNumber) (Mir_roundops.MultiRoundOps) -module IntvMfInterp = - Make - (Mir_number.IntervalNumber) - (Mir_roundops.MainframeRoundOps (MainframeLongSize)) -module RatDefInterp = - Make (Mir_number.RationalNumber) (Mir_roundops.DefaultRoundOps) -module RatMultInterp = - Make (Mir_number.RationalNumber) (Mir_roundops.MultiRoundOps) -module RatMfInterp = - Make - (Mir_number.RationalNumber) - (Mir_roundops.MainframeRoundOps (MainframeLongSize)) - -let get_interp (sort : Config.value_sort) (roundops : Config.round_ops) : - (module S) = - match (sort, roundops) with - | RegularFloat, RODefault -> (module FloatDefInterp) - | RegularFloat, ROMulti -> (module FloatMultInterp) - | RegularFloat, ROMainframe _ -> (module FloatMfInterp) - | MPFR _, RODefault -> (module MPFRDefInterp) - | MPFR _, ROMulti -> (module MPFRMultInterp) - | MPFR _, ROMainframe _ -> (module MPFRMfInterp) - | BigInt _, RODefault -> (module BigIntDefInterp) - | BigInt _, ROMulti -> (module BigIntMultInterp) - | BigInt _, ROMainframe _ -> (module BigIntMfInterp) - | Interval, RODefault -> (module IntvDefInterp) - | Interval, ROMulti -> (module IntvMultInterp) - | Interval, ROMainframe _ -> (module IntvMfInterp) - | Rational, RODefault -> (module RatDefInterp) - | Rational, ROMulti -> (module RatMultInterp) - | Rational, ROMainframe _ -> (module RatMfInterp) - -let prepare_interp (sort : Config.value_sort) (roundops : Config.round_ops) : - unit = - begin - match sort with - | MPFR prec -> Mpfr.set_default_prec prec - | BigInt prec -> BigIntPrecision.scaling_factor_bits := prec - | Interval -> Mpfr.set_default_prec 64 - | _ -> () - end; - match roundops with - | ROMainframe long_size -> - let max_long = - if long_size = 32 then Int64.of_int32 Int32.max_int - else if long_size = 64 then Int64.max_int - else assert false - (* checked when parsing command line *) - in - MainframeLongSize.max_long := max_long - | _ -> () - -let evaluate_program (p : Mir.program) (inputs : Com.literal Com.Var.Map.t) - (events : (Com.literal, Com.Var.t) Com.event_value StrMap.t list) - (sort : Config.value_sort) (roundops : Config.round_ops) : - Com.literal Com.Var.Map.t * Com.Error.Set.t = - prepare_interp sort roundops; - let module Interp = (val get_interp sort roundops : S) in - let ctx = Interp.empty_ctx p in - Interp.update_ctx_with_inputs ctx inputs; - Interp.update_ctx_with_events ctx events; - Interp.evaluate_program ctx; - Format.pp_print_flush Format.std_formatter (); - Format.pp_print_flush Format.err_formatter (); - let varMap = - let default_space = - ctx.ctx_var_spaces.(ctx.ctx_prog.program_var_space_def.vs_id) - in - let fold _ (var : Com.Var.t) res = - if Com.Var.is_given_back var || true then - let litt = - match Com.Var.cat_var_loc var with - | LocInput -> default_space.input.(Com.Var.loc_idx var) - | LocComputed -> default_space.computed.(Com.Var.loc_idx var) - | LocBase -> default_space.base.(Com.Var.loc_idx var) - in - let fVal = Interp.value_to_literal litt in - Com.Var.Map.add var fVal res - else res - in - StrMap.fold fold ctx.ctx_prog.program_vars Com.Var.Map.empty - in - let anoSet = - let fold res (e, _) = Com.Error.Set.add e res in - List.fold_left fold Com.Error.Set.empty ctx.ctx_exported_anos - in - (varMap, anoSet) - -let evaluate_expr (p : Mir.program) (e : Mir.expression Pos.marked) - (sort : Config.value_sort) (roundops : Config.round_ops) : Com.literal = - let module Interp = (val get_interp sort roundops : S) in - try Interp.value_to_literal (Interp.evaluate_expr (Interp.empty_ctx p) e) - with Stop_instruction _ -> Undefined diff --git a/src/mlang/m_ir/mir_interpreter.mli b/src/mlang/m_ir/mir_interpreter.mli deleted file mode 100644 index 81def89d4..000000000 --- a/src/mlang/m_ir/mir_interpreter.mli +++ /dev/null @@ -1,192 +0,0 @@ -(* Copyright (C) 2019-2021 Inria, contributor: Denis Merigoux - - - 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 . *) - -(** Interpretation of BIR programs *) - -(**{1 Program values}*) - -(**{1 Instrumentation of the interpreter}*) - -(** The BIR interpreter can be instrumented to record which program locations - have been executed. *) - -val exit_on_rte : bool ref -(** If set to true, the interpreter exits the whole process in case of runtime - error *) - -val repl_debug : bool ref -(** If set to true, prints the REPL debugger in case of runtime error *) - -(** {1 The interpreter functor}*) - -(** The intepreter is parametrized by the kind of floating-point values used for - the execution *) - -(** Signature of the modules produced by the functor *) -module type S = sig - type custom_float - (** Comes from the instantiation of the functor by a kind of floating-point - value *) - - (** Functor-specific program values *) - type value = Number of custom_float | Undefined - - val format_value : Format.formatter -> value -> unit - - val format_value_prec : int -> int -> Format.formatter -> value -> unit - - type ctx_tmp_var = { mutable var : Com.Var.t; mutable value : value } - - type ctx_ref_var = { - mutable var : Com.Var.t; - mutable var_space : Com.variable_space; - mutable ref_var : Com.Var.t; - mutable org : int; - } - - type print_ctx = { mutable indent : int; mutable is_newline : bool } - - type ctx_var_space = { - input : value Array.t; - computed : value Array.t; - base : value Array.t; - } - - type ctx = { - ctx_prog : Mir.program; - mutable ctx_target : Mir.target; - mutable ctx_var_space : int; - ctx_var_spaces : ctx_var_space Array.t; - ctx_tmps : ctx_tmp_var Array.t; - mutable ctx_tmps_org : int; - ctx_ref : ctx_ref_var Array.t; - mutable ctx_ref_org : int; - ctx_tab_map : Com.Var.t Array.t; - ctx_pr_out : print_ctx; - ctx_pr_err : print_ctx; - mutable ctx_anos : (Com.Error.t * string option) list; - mutable ctx_nb_anos : int; - mutable ctx_nb_discos : int; - mutable ctx_nb_infos : int; - mutable ctx_nb_bloquantes : int; - mutable ctx_archived_anos : StrSet.t; - mutable ctx_finalized_anos : (Com.Error.t * string option) list; - mutable ctx_exported_anos : (Com.Error.t * string option) list; - mutable ctx_events : (value, Com.Var.t) Com.event_value Array.t Array.t list; - } - (** Interpretation context *) - - val empty_ctx : Mir.program -> ctx - - val literal_to_value : Com.literal -> value - - val value_to_literal : value -> Com.literal - - val update_ctx_with_inputs : ctx -> Com.literal Com.Var.Map.t -> unit - - val update_ctx_with_events : - ctx -> (Com.literal, Com.Var.t) Com.event_value StrMap.t list -> unit - - (** Interpreter runtime errors *) - type run_error = - | NanOrInf of string * Mir.expression Pos.marked - | StructuredError of - (string * (string option * Pos.t) list * (unit -> unit) option) - - exception RuntimeError of run_error * ctx - - val raise_runtime_as_structured : run_error -> 'a - (** Raises a runtime error with a formatted error message and context *) - - val compare_numbers : Com.comp_op -> custom_float -> custom_float -> bool - (** Returns the comparison between two numbers in the rounding and precision - context of the interpreter. *) - - val evaluate_expr : ctx -> Mir.expression Pos.marked -> value - - val evaluate_program : ctx -> unit -end - -module FloatDefInterp : - S with type custom_float = Mir_number.RegularFloatNumber.t -(** The different interpreters, which combine a representation of numbers and - rounding operations. The first part of the name corresponds to the - representation of numbers, and is one of the following: - - - Float: "regular" IEE754 floating point numbers - - MPFR: arbitrary precision floating-point numbers using MPFR - - BigInt: fixed-point numbers - - Intv: intervals of two IEEE754 floating-point numbers - - Rat: rationals - - The second part indicates the rounding operations to use, and is one of the - following: - - - Def: use the default rounding operations, those of the PC/single-thread - context - - Multi: use the rouding operations of the PC/multi-thread context - - Mf: use the rounding operations of the mainframe context *) - -module FloatMultInterp : - S with type custom_float = Mir_number.RegularFloatNumber.t - -module FloatMfInterp : - S with type custom_float = Mir_number.RegularFloatNumber.t - -module MPFRDefInterp : S with type custom_float = Mir_number.MPFRNumber.t - -module MPFRMultInterp : S with type custom_float = Mir_number.MPFRNumber.t - -module MPFRMfInterp : S with type custom_float = Mir_number.MPFRNumber.t - -module BigIntDefInterp : S - -module BigIntMultInterp : S - -module BigIntMfInterp : S - -module IntvDefInterp : S with type custom_float = Mir_number.IntervalNumber.t - -module IntvMultInterp : S with type custom_float = Mir_number.IntervalNumber.t - -module IntvMfInterp : S with type custom_float = Mir_number.IntervalNumber.t - -module RatDefInterp : S with type custom_float = Mir_number.RationalNumber.t - -module RatMultInterp : S with type custom_float = Mir_number.RationalNumber.t - -module RatMfInterp : S with type custom_float = Mir_number.RationalNumber.t - -(** {1 Generic interpretation API}*) - -val get_interp : Config.value_sort -> Config.round_ops -> (module S) - -val evaluate_program : - Mir.program -> - Com.literal Com.Var.Map.t -> - (Com.literal, Com.Var.t) Com.event_value StrMap.t list -> - Config.value_sort -> - Config.round_ops -> - Com.literal Com.Var.Map.t * Com.Error.Set.t -(** Main interpreter function *) - -val evaluate_expr : - Mir.program -> - Mir.expression Pos.marked -> - Config.value_sort -> - Config.round_ops -> - Com.literal -(** Interprets only an expression *) diff --git a/src/mlang/m_ir/mir_number.ml b/src/mlang/m_ir/mir_number.ml index 589a261e3..3d7f2771e 100644 --- a/src/mlang/m_ir/mir_number.ml +++ b/src/mlang/m_ir/mir_number.ml @@ -14,7 +14,7 @@ You should have received a copy of the GNU General Public License along with this program. If not, see . *) -module type NumberInterface = sig +module type NumberInterfaceNoCompare = sig type t val format_t : Format.formatter -> t -> unit @@ -34,8 +34,6 @@ module type NumberInterface = sig val of_float : float -> t - val of_float_input : Com.Var.t -> float -> t - val to_float : t -> float (** Warning: lossy *) @@ -72,7 +70,30 @@ module type NumberInterface = sig val is_zero : t -> bool end -module RegularFloatNumber : NumberInterface = struct +module type NumberInterface = sig + include NumberInterfaceNoCompare + + val compare : ?epsilon:float -> Com.comp_op -> t -> t -> bool +end + +module MakeComparable (N : NumberInterfaceNoCompare) : + NumberInterface with type t = N.t = struct + include N + + let compare ?(epsilon = !Config.comparison_error_margin) op i1 i2 = + let epsilon = of_float epsilon in + let open Com in + match op with + | Gt -> i1 >. i2 +. epsilon + | Gte -> i1 >. i2 -. epsilon + | Lt -> i1 +. epsilon <. i2 + | Lte -> i1 -. epsilon <. i2 + | Eq -> abs (i1 -. i2) <. epsilon + | Neq -> abs (i1 -. i2) >=. epsilon +end + +module RegularFloatNumber : NumberInterface with type t = float = +MakeComparable (struct type t = float let format_t fmt f = Format.fprintf fmt "%f" f @@ -103,8 +124,6 @@ module RegularFloatNumber : NumberInterface = struct let of_float f = f - let of_float_input _ f = f - let to_float f = f let zero () = 0. @@ -138,7 +157,7 @@ module RegularFloatNumber : NumberInterface = struct let is_nan_or_inf x = not (Float.is_finite x) let is_zero x = x = 0. -end +end) let mpfr_abs (x : Mpfrf.t) : Mpfrf.t = let out = Mpfr.init2 (Mpfr.get_prec x) in @@ -155,7 +174,8 @@ let mpfr_ceil (x : Mpfrf.t) : Mpfrf.t = ignore (Mpfr.ceil out x); Mpfrf.of_mpfr out -module MPFRNumber : NumberInterface = struct +module MPFRNumber : NumberInterface with type t = Mpfrf.t = +MakeComparable (struct type t = Mpfrf.t let rounding : Mpfr.round = Near @@ -176,8 +196,6 @@ module MPFRNumber : NumberInterface = struct let of_float f = Mpfrf.of_float f rounding - let of_float_input _ f = Mpfrf.of_float f rounding - let to_float f = Mpfrf.to_float ~round:rounding f let zero () = Mpfrf.of_int 0 rounding @@ -214,10 +232,13 @@ module MPFRNumber : NumberInterface = struct let is_zero x = x =. zero () let is_nan_or_inf x = not (Mpfrf.number_p x) -end +end) + +type interval = { down : Mpfrf.t; up : Mpfrf.t } -module IntervalNumber : NumberInterface = struct - type t = { down : Mpfrf.t; up : Mpfrf.t } +module IntervalNumber : NumberInterface with type t = interval = +MakeComparable (struct + type t = interval let v (x : Mpfrf.t) (y : Mpfrf.t) : t = { down = x; up = y } @@ -246,9 +267,6 @@ module IntervalNumber : NumberInterface = struct let of_float (f : float) = v (Mpfrf.of_float f Down) (Mpfrf.of_float f Up) - let of_float_input (_v : Com.Var.t) (f : float) = - v (Mpfrf.of_float f Down) (Mpfrf.of_float f Up) - let to_float (f : t) : float = let fd = Mpfrf.to_float ~round:Down f.down in let fu = Mpfrf.to_float ~round:Up f.up in @@ -335,9 +353,10 @@ module IntervalNumber : NumberInterface = struct let is_zero x = x =. zero () let is_nan_or_inf x = not (Mpfrf.number_p x.down && Mpfrf.number_p x.up) -end +end) -module RationalNumber : NumberInterface = struct +module RationalNumber : NumberInterface with type t = Mpqf.t = +MakeComparable (struct type t = Mpqf.t let format_t fmt f = Mpqf.print fmt f @@ -362,8 +381,6 @@ module RationalNumber : NumberInterface = struct let of_float f = Mpqf.of_float f - let of_float_input _ f = Mpqf.of_float f - let to_float f = Mpqf.to_float f let zero () = Mpqf.of_int 0 @@ -407,11 +424,11 @@ module RationalNumber : NumberInterface = struct || Mpzf.cmp (Mpqf.get_den x) max > 0 || Mpzf.cmp (Mpqf.get_num x) min < 0 || Mpzf.cmp (Mpqf.get_den x) min < 0 -end +end) module BigIntFixedPointNumber (P : sig val scaling_factor_bits : int ref -end) : NumberInterface = struct +end) : NumberInterface with type t = Mpzf.t = MakeComparable (struct type t = Mpzf.t let precision_modulo () = @@ -457,8 +474,6 @@ end) : NumberInterface = struct (Mpzf.of_float frac_part_scaled) (Mpzf.mul (Mpzf.of_float int_part) (precision_modulo ())) - let of_float_input _ (f : float) : t = of_float f - let to_float f = let frac_part, int_part = modf f in Mpzf.to_float (Mpzf.tdiv_q int_part (precision_modulo ())) @@ -498,4 +513,4 @@ end) : NumberInterface = struct let max x y = if x >. y then x else y let is_nan_or_inf _ = false -end +end) diff --git a/src/mlang/m_ir/mir_number.mli b/src/mlang/m_ir/mir_number.mli index af66b405c..e9f804f47 100644 --- a/src/mlang/m_ir/mir_number.mli +++ b/src/mlang/m_ir/mir_number.mli @@ -14,6 +14,8 @@ You should have received a copy of the GNU General Public License along with this program. If not, see . *) +type interval = { down : Mpfrf.t; up : Mpfrf.t } + module type NumberInterface = sig type t @@ -33,8 +35,6 @@ module type NumberInterface = sig val of_float : float -> t - val of_float_input : Com.Var.t -> float -> t - val to_float : t -> float val zero : unit -> t @@ -68,20 +68,24 @@ module type NumberInterface = sig val is_nan_or_inf : t -> bool val is_zero : t -> bool + + val compare : ?epsilon:float -> Com.comp_op -> t -> t -> bool + (** Returns the comparison between two numbers in the precision context of the + current configuration. *) end -module RegularFloatNumber : NumberInterface +module RegularFloatNumber : NumberInterface with type t = float val mpfr_floor : Mpfrf.t -> Mpfrf.t -module MPFRNumber : NumberInterface +module MPFRNumber : NumberInterface with type t = Mpfrf.t -module IntervalNumber : NumberInterface +module IntervalNumber : NumberInterface with type t = interval -module RationalNumber : NumberInterface +module RationalNumber : NumberInterface with type t = Mpqf.t module BigIntFixedPointNumber : functor (P : sig val scaling_factor_bits : int ref end) - -> NumberInterface + -> NumberInterface with type t = Mpzf.t diff --git a/src/mlang/mir_interpreter/anomalies.ml b/src/mlang/mir_interpreter/anomalies.ml new file mode 100644 index 000000000..c4a7e1f14 --- /dev/null +++ b/src/mlang/mir_interpreter/anomalies.ml @@ -0,0 +1,77 @@ +open Types + +let raise ctx err v_opt = + (match err.Com.Error.typ with + | Com.Error.Anomaly -> ctx.ctx_nb_anos <- ctx.ctx_nb_anos + 1 + | Com.Error.Discordance -> ctx.ctx_nb_discos <- ctx.ctx_nb_discos + 1 + | Com.Error.Information -> ctx.ctx_nb_infos <- ctx.ctx_nb_infos + 1); + let is_blocking = + err.typ = Com.Error.Anomaly && Pos.unmark err.is_isf = "N" + in + ctx.ctx_nb_bloquantes <- (ctx.ctx_nb_bloquantes + if is_blocking then 1 else 0); + ctx.ctx_anos <- ctx.ctx_anos @ [ (err, v_opt) ]; + is_blocking + +let clean (ctx : 'a ctx) = + ctx.ctx_anos <- []; + ctx.ctx_nb_anos <- 0; + ctx.ctx_nb_discos <- 0; + ctx.ctx_nb_infos <- 0; + ctx.ctx_nb_bloquantes <- 0 + +let clean_finalized (ctx : 'a ctx) = ctx.ctx_finalized_anos <- [] + +let finalize ~mode_corr (ctx : 'a ctx) = + let mem (ano : Com.Error.t) anos = + List.fold_left + (fun res ((a : Com.Error.t), _) -> + res || Pos.unmark a.name = Pos.unmark ano.name) + false anos + in + if mode_corr then + let rec merge_anos () = + match ctx.ctx_anos with + | [] -> () + | ((ano : Com.Error.t), arg) :: discos -> + let cont = + if not (mem ano ctx.ctx_finalized_anos) then ( + ctx.ctx_finalized_anos <- ctx.ctx_finalized_anos @ [ (ano, arg) ]; + ano.typ <> Com.Error.Anomaly) + else true + in + ctx.ctx_anos <- discos; + if cont then merge_anos () + in + merge_anos () + else ( + clean_finalized ctx; + let rec merge_anos () = + match ctx.ctx_anos with + | [] -> ctx.ctx_finalized_anos <- List.rev ctx.ctx_finalized_anos + | ((ano : Com.Error.t), arg) :: discos -> + if not (StrSet.mem (Pos.unmark ano.name) ctx.ctx_archived_anos) then ( + ctx.ctx_archived_anos <- + StrSet.add (Pos.unmark ano.name) ctx.ctx_archived_anos; + ctx.ctx_finalized_anos <- (ano, arg) :: ctx.ctx_finalized_anos); + ctx.ctx_anos <- discos; + merge_anos () + in + merge_anos ()) + +let export ~mode_corr (ctx : 'a ctx) = + if mode_corr then + let rec merge_anos () = + match ctx.ctx_finalized_anos with + | [] -> () + | ((ano : Com.Error.t), arg) :: fins -> + if not (StrSet.mem (Pos.unmark ano.name) ctx.ctx_archived_anos) then ( + ctx.ctx_archived_anos <- + StrSet.add (Pos.unmark ano.name) ctx.ctx_archived_anos; + ctx.ctx_exported_anos <- ctx.ctx_exported_anos @ [ (ano, arg) ]); + ctx.ctx_finalized_anos <- fins; + merge_anos () + in + merge_anos () + else ( + ctx.ctx_exported_anos <- ctx.ctx_exported_anos @ ctx.ctx_finalized_anos; + clean_finalized ctx) diff --git a/src/mlang/mir_interpreter/anomalies.mli b/src/mlang/mir_interpreter/anomalies.mli new file mode 100644 index 000000000..f2b65081f --- /dev/null +++ b/src/mlang/mir_interpreter/anomalies.mli @@ -0,0 +1,17 @@ +val raise : 'a Types.ctx -> M_ir.Com.Error.t -> string option -> bool +(** Adds the anomaly to the context and returns [true] if the said anomaly is + blocking, [false] otherwise. *) + +val clean : 'a Types.ctx -> unit +(** Cleans the context from its unfinalized and unarchived anomalies. *) + +val clean_finalized : 'a Types.ctx -> unit +(** Cleans the context from its finalized anomalies. *) + +val finalize : mode_corr:bool -> 'a Types.ctx -> unit +(** Moves the raised anomalies to the finalized anomalies (and the archived + anomalies if [mode_corr] is [true]). *) + +val export : mode_corr:bool -> 'a Types.ctx -> unit +(** Moves the finalized anomalies to the exported anomalies (and the archived + anomalies if [mode_corr] is [true]). *) diff --git a/src/mlang/mir_interpreter/context.ml b/src/mlang/mir_interpreter/context.ml new file mode 100644 index 000000000..606db34d3 --- /dev/null +++ b/src/mlang/mir_interpreter/context.ml @@ -0,0 +1,410 @@ +open Types + +module type S = sig + type custom_float + + val get_var_space : + custom_float Types.ctx -> M_ir.Com.var_space -> M_ir.Com.variable_space + + val get_var : + custom_float Types.ctx -> + M_ir.Com.var_space -> + M_ir.Com.Var.t -> + M_ir.Com.variable_space * M_ir.Com.Var.t * int + + val get_var_tab : + custom_float Types.ctx -> M_ir.Com.Var.t -> int -> M_ir.Com.Var.t + + val get_var_value_org : + custom_float Types.ctx -> + M_ir.Com.variable_space -> + M_ir.Com.Var.t -> + int -> + custom_float Types.value + + val get_var_value : + custom_float Types.ctx -> + M_ir.Com.var_space -> + M_ir.Com.Var.t -> + custom_float Types.value + + val get_var_value_tab : + custom_float Types.ctx -> + M_ir.Com.var_space -> + M_ir.Com.Var.t -> + int -> + custom_float Types.value + + val set_var_ref : + custom_float Types.ctx -> + M_ir.Com.Var.t -> + M_ir.Com.variable_space -> + M_ir.Com.Var.t -> + int -> + unit + + val get_access_value : + eval: + (custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.m_expression -> + custom_float Types.value) -> + custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.access -> + custom_float Types.value + + val get_access_var : + eval: + (custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.m_expression -> + custom_float Types.value) -> + custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.access -> + (M_ir.Com.variable_space * M_ir.Com.Var.t * int) option + + val set_var_value_org : + custom_float Types.ctx -> + M_ir.Com.variable_space -> + M_ir.Com.Var.t -> + int -> + custom_float Types.value -> + unit + + val set_var_value : + custom_float Types.ctx -> + M_ir.Com.var_space -> + M_ir.Com.Var.t -> + custom_float Types.value -> + unit + + val set_var_value_tab : + custom_float Types.ctx -> + M_ir.Com.var_space -> + M_ir.Com.Var.t -> + int -> + custom_float Types.value -> + unit + + val set_access : + eval: + (custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.m_expression -> + custom_float Types.value) -> + custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.access -> + custom_float Types.value -> + unit +end + +let update_ctx_with_inputs (ctx : 'a ctx) + (value_inputs : 'a value Com.Var.Map.t) : unit = + (* let value_inputs = *) + (* Com.Var.Map.mapi *) + (* (fun v l -> *) + (* match l with *) + (* | Com.Undefined -> Undefined *) + (* | Com.Float f -> Number (N.of_float_input v f)) *) + (* inputs *) + (* in *) + let default_space = + ctx.ctx_var_spaces.(ctx.ctx_prog.program_var_space_def.vs_id) + in + Com.Var.Map.iter + (fun (var : Com.Var.t) value -> + match Com.Var.cat_var_loc var with + | LocInput -> default_space.input.(Com.Var.loc_idx var) <- value + | LocComputed -> default_space.computed.(Com.Var.loc_idx var) <- value + | LocBase -> default_space.base.(Com.Var.loc_idx var) <- value) + value_inputs + +let update_ctx_with_events (ctx : 'a ctx) + (events : ('a value, Com.Var.t) Com.event_value StrMap.t list) : unit = + let nbEvt = List.length events in + let ctx_event_tab = Array.make nbEvt [||] in + let fold idx (evt : ('a value, Com.Var.t) Com.event_value StrMap.t) = + let nbProgFields = StrMap.cardinal ctx.ctx_prog.program_event_fields in + let map = Array.make nbProgFields (Com.Numeric Undefined) in + for id = 0 to nbProgFields - 1 do + let fname = IntMap.find id ctx.ctx_prog.program_event_field_idxs in + let ef = StrMap.find fname ctx.ctx_prog.program_event_fields in + if ef.is_var then + map.(id) <- + Com.RefVar (snd (StrMap.min_binding ctx.ctx_prog.program_vars)) + done; + let iter' fname ev = + match StrMap.find_opt fname ctx.ctx_prog.program_event_fields with + | Some ef -> ( + match (ev, ef.is_var) with + | Com.Numeric _, false | Com.RefVar _, true -> map.(ef.index) <- ev + | _ -> Errors.raise_error "wrong event field type") + | None -> Errors.raise_error "unknown event field" + in + StrMap.iter iter' evt; + ctx_event_tab.(idx) <- map; + idx + 1 + in + ignore (List.fold_left fold 0 events); + (* let max_field_length = + StrMap.fold + (fun s _ r -> max r (String.length s)) + ctx.ctx_prog.program_event_fields 0 + in + let pp_field fmt s = + let l = String.length s in + Format.fprintf fmt "%s%s" s (String.make (max_field_length - l + 1) ' ') + in + let pp_ev fmt = function + | Com.Numeric Undefined -> Pp.string fmt "indefini" + | Com.Numeric (Number v) -> N.format_t fmt v + | Com.RefVar v -> Pp.string fmt (Com.Var.name_str v) + in + for i = 0 to Array.length ctx_event_tab - 1 do + Format.eprintf "%d@." i; + let map = ctx_event_tab.(i) in + for j = 0 to Array.length map - 1 do + let s = IntMap.find j ctx.ctx_prog.program_event_field_idxs in + Format.eprintf " %a%a@." pp_field s pp_ev map.(j) + done + done;*) + ctx.ctx_events <- [ ctx_event_tab ] + +let empty_ctx ?inputs ?events (p : M_ir.Mir.program) : 'a ctx = + let dummy_var = Com.Var.new_ref ~name:(Pos.without "") in + let init_tmp_var _i = { var = dummy_var; value = Undefined } in + let init_ref _i = + { + var = dummy_var; + var_space = p.program_var_space_def; + ref_var = dummy_var; + org = -1; + } + in + let ctx_tab_map = + let init i = IntMap.find i p.program_stats.table_map in + Array.init (IntMap.cardinal p.program_stats.table_map) init + in + let ctx_var_spaces = + let init i = + let vsd = IntMap.find i p.program_var_spaces_idx in + let input = + if Com.CatVar.LocMap.mem Com.CatVar.LocInput vsd.vs_cats then + Array.make p.program_stats.sz_input Undefined + else Array.make 0 Undefined + in + let computed = + if Com.CatVar.LocMap.mem Com.CatVar.LocComputed vsd.vs_cats then + Array.make p.program_stats.sz_computed Undefined + else Array.make 0 Undefined + in + let base = + if Com.CatVar.LocMap.mem Com.CatVar.LocBase vsd.vs_cats then + Array.make p.program_stats.sz_base Undefined + else Array.make 0 Undefined + in + { input; computed; base } + in + Array.init (IntMap.cardinal p.program_var_spaces_idx) init + in + let res = + { + ctx_prog = p; + ctx_target = snd (StrMap.min_binding p.program_targets); + ctx_var_space = p.program_var_space_def.vs_id; + ctx_var_spaces; + ctx_tmps = Array.init p.program_stats.sz_all_tmps init_tmp_var; + ctx_tmps_org = 0; + ctx_ref = Array.init p.program_stats.nb_all_refs init_ref; + ctx_ref_org = 0; + ctx_tab_map; + ctx_pr_out = { indent = 0; is_newline = true }; + ctx_pr_err = { indent = 0; is_newline = true }; + ctx_anos = []; + ctx_nb_anos = 0; + ctx_nb_discos = 0; + ctx_nb_infos = 0; + ctx_nb_bloquantes = 0; + ctx_archived_anos = StrSet.empty; + ctx_finalized_anos = []; + ctx_exported_anos = []; + ctx_events = []; + } + in + Option.iter (update_ctx_with_inputs res) inputs; + Option.iter (update_ctx_with_events res) events; + res + +module Make (N : Number.S) = struct + let get_var_space (ctx : N.t ctx) (m_sp_opt : Com.var_space) = + let i_sp = + match m_sp_opt with None -> ctx.ctx_var_space | Some (_, i_sp) -> i_sp + in + IntMap.find i_sp ctx.ctx_prog.program_var_spaces_idx + + let get_var (ctx : N.t ctx) (m_sp_opt : Com.var_space) (var : Com.Var.t) : + Com.variable_space * Com.Var.t * int = + match var.scope with + | Com.Var.Tgv _ -> (get_var_space ctx m_sp_opt, var, 0) + | Com.Var.Temp _ -> (get_var_space ctx None, var, ctx.ctx_tmps_org) + | Com.Var.Ref -> + let rv = ctx.ctx_ref.(ctx.ctx_ref_org + Com.Var.loc_idx var) in + let vsd = + match m_sp_opt with + | None -> rv.var_space + | _ -> get_var_space ctx m_sp_opt + in + (vsd, rv.ref_var, rv.org) + + let get_var_tab (ctx : N.t ctx) (var : Com.Var.t) (i : int) : Com.Var.t = + match Com.Var.get_table var with + | Some _ -> ctx.ctx_tab_map.(Com.Var.loc_tab_idx var + 1 + i) + | None -> assert false + + let get_var_value_org (ctx : N.t ctx) (vsd : Com.variable_space) + (var : Com.Var.t) (vorg : int) : N.t value = + let vi = Com.Var.loc_idx var in + match var.scope with + | Com.Var.Tgv _ -> + let var_space = ctx.ctx_var_spaces.(vsd.vs_id) in + let var_tab = + match Com.Var.cat_var_loc var with + | LocInput -> var_space.input + | LocComputed -> var_space.computed + | LocBase -> var_space.base + in + if Array.length var_tab > 0 then var_tab.(vi) else Undefined + | Com.Var.Temp _ -> ctx.ctx_tmps.(vorg + vi).value + | Com.Var.Ref -> assert false + + let get_var_value (ctx : N.t ctx) (m_sp_opt : Com.var_space) (v : Com.Var.t) : + N.t value = + let vsd, var, vorg = get_var ctx m_sp_opt v in + let var = if Com.Var.is_table var then get_var_tab ctx var 0 else var in + get_var_value_org ctx vsd var vorg + + let get_var_value_tab (ctx : N.t ctx) (m_sp_opt : Com.var_space) + (v : Com.Var.t) (i : int) : N.t value = + let vsd, var, vorg = get_var ctx m_sp_opt v in + if i < 0 then Number (N.zero ()) + else if Com.Var.size var <= i then Undefined + else if Com.Var.is_table var then + let var_i = get_var_tab ctx var i in + get_var_value_org ctx vsd var_i vorg + else get_var_value_org ctx vsd var vorg + + let set_var_ref (ctx : N.t ctx) (var : Com.Var.t) + (var_space : Com.variable_space) (ref_var : Com.Var.t) (org : int) : unit + = + match var.loc with + | LocRef (_, i) -> + ctx.ctx_ref.(ctx.ctx_ref_org + i).var <- var; + ctx.ctx_ref.(ctx.ctx_ref_org + i).var_space <- var_space; + ctx.ctx_ref.(ctx.ctx_ref_org + i).ref_var <- ref_var; + ctx.ctx_ref.(ctx.ctx_ref_org + i).org <- org + | _ -> assert false + + let rec get_access_value ~eval ctx access = + match access with + | Com.VarAccess (m_sp_opt, v) -> get_var_value ctx m_sp_opt v + | Com.TabAccess ((m_sp_opt, v), m_idx) -> ( + match eval ctx m_idx with + | Number z -> + let i = Int64.to_int @@ N.to_int z in + get_var_value_tab ctx m_sp_opt v i + | Undefined -> Undefined) + | Com.FieldAccess (m_sp_opt, e, _, j) -> ( + match eval ctx e with + | Number z -> + let i = Int64.to_int @@ N.to_int z in + let events = List.hd ctx.ctx_events in + if 0 <= i && i < Array.length events then + match events.(i).(j) with + | Com.Numeric n -> n + | Com.RefVar v -> get_var_value ctx m_sp_opt v + else Undefined + | Undefined -> Undefined) + + and get_access_var ~eval ctx access = + match access with + | Com.VarAccess (m_sp_opt, v) -> + let vsd, v, vorg = get_var ctx m_sp_opt v in + Some (vsd, v, vorg) + | Com.TabAccess ((m_sp_opt, m_v), m_i) -> ( + match eval ctx m_i with + | Number z -> + let vsd, v, vorg = get_var ctx m_sp_opt m_v in + let i = Int64.to_int @@ N.to_int z in + if 0 <= i && i < Com.Var.size v then + if Com.Var.is_table v then + let v_i = get_var_tab ctx v i in + Some (vsd, v_i, vorg) + else Some (vsd, v, vorg) + else None + | Undefined -> None) + | Com.FieldAccess (m_sp_opt, m_e, _, j) -> ( + match eval ctx m_e with + | Number z -> + let i = Int64.to_int @@ N.to_int z in + let events = List.hd ctx.ctx_events in + if 0 <= i && i < Array.length events then + match events.(i).(j) with + | Com.RefVar v -> + let vsd, var, vorg = get_var ctx m_sp_opt v in + Some (vsd, var, vorg) + | Com.Numeric _ -> None + else None + | _ -> None) + + and set_var_value_org (ctx : N.t ctx) (vsd : Com.variable_space) + (var : Com.Var.t) (vorg : int) (value : N.t value) : unit = + let vi = Com.Var.loc_idx var in + match var.scope with + | Com.Var.Tgv _ -> + let var_space = ctx.ctx_var_spaces.(vsd.vs_id) in + let var_tab = + match Com.Var.cat_var_loc var with + | LocInput -> var_space.input + | LocComputed -> var_space.computed + | LocBase -> var_space.base + in + if Array.length var_tab > 0 then var_tab.(vi) <- value + | Com.Var.Temp _ -> ctx.ctx_tmps.(vorg + vi).value <- value + | Com.Var.Ref -> assert false + + and set_var_value (ctx : N.t ctx) (m_sp_opt : Com.var_space) (var : Com.Var.t) + (value : N.t value) : unit = + let vsd, v, vorg = get_var ctx m_sp_opt var in + if Com.Var.is_table v then + for i = 0 to Com.Var.size v - 1 do + let v_i = get_var_tab ctx v i in + set_var_value_org ctx vsd v_i vorg value + done + else set_var_value_org ctx vsd v vorg value + + and set_var_value_tab (ctx : N.t ctx) (m_sp_opt : Com.var_space) + (v : Com.Var.t) (i : int) (value : N.t value) : unit = + let vsd, var, vorg = get_var ctx m_sp_opt v in + if 0 <= i && i < Com.Var.size var then + if Com.Var.is_table var then + let var_i = get_var_tab ctx var i in + set_var_value_org ctx vsd var_i vorg value + else set_var_value_org ctx vsd var vorg value + + and set_access ~eval ctx access value = + match access with + | Com.VarAccess (m_sp_opt, v) -> set_var_value ctx m_sp_opt v value + | Com.TabAccess ((m_sp_opt, v), m_idx) -> ( + match eval ctx m_idx with + | Number z -> + let i = Int64.to_int @@ N.to_int z in + set_var_value_tab ctx m_sp_opt v i value + | Undefined -> ()) + | Com.FieldAccess (m_sp_opt, e, _, j) -> ( + match eval ctx e with + | Number z -> ( + let i = Int64.to_int @@ N.to_int z in + let events = List.hd ctx.ctx_events in + if 0 <= i && i < Array.length events then + match events.(i).(j) with + | Com.Numeric _ -> events.(i).(j) <- Com.Numeric value + | Com.RefVar v -> set_var_value ctx m_sp_opt v value) + | Undefined -> ()) +end diff --git a/src/mlang/mir_interpreter/context.mli b/src/mlang/mir_interpreter/context.mli new file mode 100644 index 000000000..c6fb0e01c --- /dev/null +++ b/src/mlang/mir_interpreter/context.mli @@ -0,0 +1,114 @@ +module type S = sig + type custom_float + + val get_var_space : + custom_float Types.ctx -> M_ir.Com.var_space -> M_ir.Com.variable_space + (** Returns the variable space of a given variable. *) + + val get_var : + custom_float Types.ctx -> + M_ir.Com.var_space -> + M_ir.Com.Var.t -> + M_ir.Com.variable_space * M_ir.Com.Var.t * int + (** Returns the variable identifier and its space, with an offset integer. + This offset integer is 0 for TGV variables *) + + val get_var_tab : + custom_float Types.ctx -> M_ir.Com.Var.t -> int -> M_ir.Com.Var.t + (** [get_var_tab ctx vs v i] Each cell of a table is a separate variable. This + function returns the variable representing the cell [i] in table [v]. + Fails if the variable in argument is not a table. *) + + val get_var_value_org : + custom_float Types.ctx -> + M_ir.Com.variable_space -> + M_ir.Com.Var.t -> + int -> + custom_float Types.value + (** *) + + val get_var_value : + custom_float Types.ctx -> + M_ir.Com.var_space -> + M_ir.Com.Var.t -> + custom_float Types.value + + val get_var_value_tab : + custom_float Types.ctx -> + M_ir.Com.var_space -> + M_ir.Com.Var.t -> + int -> + custom_float Types.value + + val set_var_ref : + custom_float Types.ctx -> + M_ir.Com.Var.t -> + M_ir.Com.variable_space -> + M_ir.Com.Var.t -> + int -> + unit + + val get_access_value : + eval: + (custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.m_expression -> + custom_float Types.value) -> + custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.access -> + custom_float Types.value + + val get_access_var : + eval: + (custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.m_expression -> + custom_float Types.value) -> + custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.access -> + (M_ir.Com.variable_space * M_ir.Com.Var.t * int) option + + val set_var_value_org : + custom_float Types.ctx -> + M_ir.Com.variable_space -> + M_ir.Com.Var.t -> + int -> + custom_float Types.value -> + unit + + val set_var_value : + custom_float Types.ctx -> + M_ir.Com.var_space -> + M_ir.Com.Var.t -> + custom_float Types.value -> + unit + + val set_var_value_tab : + custom_float Types.ctx -> + M_ir.Com.var_space -> + M_ir.Com.Var.t -> + int -> + custom_float Types.value -> + unit + + val set_access : + eval: + (custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.m_expression -> + custom_float Types.value) -> + custom_float Types.ctx -> + M_ir.Com.Var.t M_ir.Com.access -> + custom_float Types.value -> + unit +end + +val empty_ctx : + ?inputs:'a Types.value M_ir.Com.Var.Map.t -> + ?events:('a Types.value, M_ir.Com.Var.t) M_ir.Com.event_value StrMap.t list -> + M_ir.Mir.program -> + 'a Types.ctx +(** [empty_ctx ?inputs ?events p] + + Creates a fresh context for executing the program [p] or expressions within + the context of [p] (for example, with variables declared in [p]. Parameters + [inputs] and [events] are required for interpreting the whole program. *) + +module Make (N : Number.S) : S with type custom_float := N.t diff --git a/src/mlang/mir_interpreter/dune b/src/mlang/mir_interpreter/dune new file mode 100644 index 000000000..1212300e7 --- /dev/null +++ b/src/mlang/mir_interpreter/dune @@ -0,0 +1,6 @@ +(library + (public_name mlang.interpreter) + (name m_interpreter) + (flags + (:standard -open Utils)) + (libraries utils m_ir num gmp re)) diff --git a/src/mlang/mir_interpreter/eval.ml b/src/mlang/mir_interpreter/eval.ml new file mode 100644 index 000000000..cd8dd65e5 --- /dev/null +++ b/src/mlang/mir_interpreter/eval.ml @@ -0,0 +1,881 @@ +(* Copyright (C) 2019-2021 Inria, contributor: Denis Merigoux + + + 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 . *) + +open M_ir +open Types + +exception Stop_instruction of Com.stop_kind + +let exit_on_rte = ref true + +module type S = sig + type custom_float + + type nonrec ctx = custom_float ctx + + exception InternalRuntimeError of run_error * ctx + + (** {2 M Evaluation} *) + + val evaluate_expr : + ctx -> M_ir.Mir.expression Pos.marked -> custom_float value + (** Evaluates an expression. *) + + val evaluate_program : ctx -> unit + (** Evaluates a whole program. Proper initialisation of inputs and events is + required before calling this function (through [update_ctx_with_inputs] + and [update_ctx_with_events]. *) + + (** {2 Helpers} *) + + (** These helpers are here for compatibility with {!module: Context}. *) + + val literal_to_value : Com.literal -> custom_float value + + val value_to_literal : custom_float value -> Com.literal + + val literal_event_to_value_event : + (Com.literal, Com.Var.t) Com.event_value -> + (custom_float value, Com.Var.t) Com.event_value +end + +module Make (N : Types.Number) : S with type custom_float = N.t = struct + (* Careful : this behavior mimics the one imposed by the original Mlang + compiler... *) + + module Funs = Functions.Make (N) + module C = Context.Make (N) + module Print = Print.Make (N) + + type custom_float = N.t + + type nonrec value = custom_float value + + type nonrec ctx = custom_float ctx + + exception InternalRuntimeError of run_error * ctx + + exception BlockingError + + let roundf (x : N.t) = N.roundf x + + let literal_to_value (l : Com.literal) : value = + match l with + | Com.Undefined -> Undefined + | Com.Float f -> Number (N.of_float f) + + let value_to_literal (l : value) : Com.literal = + match l with + | Undefined -> Com.Undefined + | Number f -> Com.Float (N.to_float f) + + let literal_event_to_value_event = function + | Com.Numeric Com.Undefined -> Com.Numeric Undefined + | Com.Numeric (Com.Float f) -> Com.Numeric (Number (N.of_float f)) + | Com.RefVar v -> Com.RefVar v + + let raise_runtime_as_structured (e : run_error) = + match e with + | NanOrInf (v, e) -> + Errors.raise_spanned_error + (Format.asprintf "Expression evaluated to %s: %a" v + Format_mir.format_expression (Pos.unmark e)) + (Pos.get e) + | StructuredError (msg, pos, kont) -> + raise (Errors.StructuredError (msg, pos, kont)) + + let is_zero (l : value) : bool = + match l with Number z -> N.is_zero z | _ -> false + + let real_of_bool (b : bool) = if b then N.one () else N.zero () + + let bool_of_real (f : N.t) : bool = not N.(f =. zero ()) + + let mode_corr (ctx : ctx) = + match StrMap.find_opt "MODE_CORR" ctx.ctx_prog.program_vars with + | Some var -> ( + let vsd = ctx.ctx_prog.program_var_space_def in + let _, var, vorg = C.get_var ctx None var in + match C.get_var_value_org ctx vsd var vorg with + | Undefined -> false + | Number n -> N.compare Eq n (N.one ())) + | None -> false + + let comparison op new_e1 new_e2 = + match (op, new_e1, new_e2) with + | Com.(Gt | Gte | Lt | Lte | Eq | Neq), _, Undefined + | Com.(Gt | Gte | Lt | Lte | Eq | Neq), Undefined, _ -> + Undefined + | op, Number i1, Number i2 -> Number (real_of_bool @@ N.compare op i1 i2) + + let unop op new_e1 = + match (op, new_e1) with + | Com.Not, Number b1 -> Number (real_of_bool (not (bool_of_real b1))) + | Minus, Number f1 -> Number N.(zero () -. f1) + | (Not | Minus), Undefined -> Undefined + + let binop (op : Com.binop) new_e1 new_e2 = + match (op, new_e1, new_e2) with + | Add, Number i1, Number i2 -> Number N.(i1 +. i2) + | Add, Number i1, Undefined -> Number N.(i1 +. zero ()) + | Add, Undefined, Number i2 -> Number N.(zero () +. i2) + | Add, Undefined, Undefined -> Undefined + | Sub, Number i1, Number i2 -> Number N.(i1 -. i2) + | Sub, Number i1, Undefined -> Number N.(i1 -. zero ()) + | Sub, Undefined, Number i2 -> Number N.(zero () -. i2) + | Sub, Undefined, Undefined -> Undefined + | Mul, _, Undefined | Mul, Undefined, _ -> Undefined + | Mul, Number i1, Number i2 -> Number N.(i1 *. i2) + | Div, Undefined, _ | Div, _, Undefined -> Undefined + | Div, _, l2 when is_zero l2 -> Number (N.zero ()) (* yes... *) + | Div, Number i1, Number i2 -> Number N.(i1 /. i2) + | Mod, Undefined, _ | Mod, _, Undefined -> Undefined + | Mod, _, l2 when is_zero l2 -> Number (N.zero ()) (* yes... *) + | Mod, Number i1, Number i2 -> Number N.(i1 %. i2) + | And, Undefined, _ | And, _, Undefined -> Undefined + | Or, Undefined, Undefined -> Undefined + | Or, Undefined, Number i | Or, Number i, Undefined -> Number i + | And, Number i1, Number i2 -> + Number (real_of_bool (bool_of_real i1 && bool_of_real i2)) + | Or, Number i1, Number i2 -> + Number (real_of_bool (bool_of_real i1 || bool_of_real i2)) + + let rec same_variable ctx m_acc m_acc' : bool = + let v0_opt = C.get_access_var ~eval:evaluate_expr ctx (Pos.unmark m_acc) in + let v1_opt = C.get_access_var ~eval:evaluate_expr ctx (Pos.unmark m_acc') in + match (v0_opt, v1_opt) with + | Some (_, v0, _), Some (_, v1, _) -> + Com.Var.name_str v0 = Com.Var.name_str v1 + | _, _ -> false + + and evaluate_switch_expr (ctx : ctx) s_e = + match s_e with + | Com.SEValue e -> ( + match evaluate_expr ctx e with + | Undefined -> `Undefined + | Number n -> `Value n) + | SESameVariable v -> `Var v + + and in_set ctx positive value0 values = + let or_chain = + List.fold_left + (fun or_chain set_value -> + let equal_test = + match set_value with + | Com.VarValue (Pos.Mark (access, _)) -> + let value = C.get_access_value ~eval:evaluate_expr ctx access in + comparison Com.Eq value0 value + | Com.FloatValue i -> + let value_i = Number (N.of_float @@ Pos.unmark i) in + comparison Com.Eq value0 value_i + | Com.IntervalValue (bn, en) -> + let value_bn = + Number (N.of_float @@ float_of_int @@ Pos.unmark bn) + in + let value_en = + Number (N.of_float @@ float_of_int @@ Pos.unmark en) + in + binop Com.And + (comparison Com.Gte value0 value_bn) + (comparison Com.Lte value0 value_en) + in + binop Com.Or or_chain equal_test) + Undefined values + in + if positive then or_chain else unop Com.Not or_chain + + and cond ctx cond th el = + match evaluate_expr ctx cond with + | Number z when N.(z =. zero ()) -> ( + match el with None -> Undefined | Some e -> evaluate_expr ctx e) + | Number _ -> evaluate_expr ctx th + | Undefined -> Undefined + + and get_attr ctx m_acc attr = + match C.get_access_var ~eval:evaluate_expr ctx (Pos.unmark m_acc) with + | Some (_, v, _) -> ( + match StrMap.find_opt (Pos.unmark attr) (Com.Var.attrs v) with + | Some l -> Number (N.of_float (float (Pos.unmark l))) + | None -> Undefined) + | None -> Undefined + + and get_size ctx m_acc = + match C.get_access_var ~eval:evaluate_expr ctx (Pos.unmark m_acc) with + | Some (_, v, _) -> Number (N.of_float @@ float @@ Com.Var.size v) + | None -> Undefined + + and get_type ctx m_acc m_typ = + match C.get_access_var ~eval:evaluate_expr ctx (Pos.unmark m_acc) with + | Some (_, v, _) -> + if Com.Var.is_tgv v && Com.Var.typ v = Some (Pos.unmark m_typ) then + Number (N.one ()) + else Number (N.zero ()) + | None -> Undefined + + and in_domain ctx m_acc dom = + match C.get_access_var ~eval:evaluate_expr ctx (Pos.unmark m_acc) with + | Some (_, v, _) -> + if Com.Var.is_tgv v && Com.CatVar.Map.mem (Com.Var.cat v) dom then + Number (N.one ()) + else Number (N.zero ()) + | None -> Number (N.zero ()) + + and evaluate_assign (ctx : ctx) = function + | Com.SingleFormula (VarDecl (m_acc, vexpr)) -> + C.set_access ~eval:evaluate_expr ctx (Pos.unmark m_acc) + @@ evaluate_expr ctx vexpr + | SingleFormula (EventFieldRef (idx, _, j, var)) -> ( + match evaluate_expr ctx idx with + | Number z when N.(z >=. zero ()) -> ( + let i = Int64.to_int @@ N.to_int z in + let events = List.hd ctx.ctx_events in + if 0 <= i && i < Array.length events then + match events.(i).(j) with + | Com.RefVar _ -> + let _, v, _ = C.get_var ctx None var in + if Com.Var.is_tgv v && not (Com.Var.is_table v) then + events.(i).(j) <- Com.RefVar v + | Com.Numeric _ -> ()) + | _ -> ()) + | Com.MultipleFormulaes _ -> assert false + + and evaluate_ite canBlock ctx b t f = + match evaluate_expr ctx b with + | Number z when N.(z =. zero ()) -> evaluate_stmts canBlock ctx f + | Number _ -> evaluate_stmts canBlock ctx t + | Undefined -> () + + and evaluate_switch = + let exception INTERNAL_STOP_SWITCH in + let then_ () = raise INTERNAL_STOP_SWITCH in + fun canBlock ctx c l -> + let v = evaluate_switch_expr ctx c in + let default = ref None in + try + List.iter + (fun (cases, stmts) -> + List.iter + (fun case -> + match (case, v) with + | Com.CDefault, _ -> + (* Trigged only if all other cases fail *) + default := Some stmts + | CValue Undefined, `Undefined -> + evaluate_stmts ~then_ canBlock ctx stmts + | CValue _, `Undefined | CValue Undefined, _ -> () + | CValue (Float f), `Value v -> + if N.of_float f = v then + evaluate_stmts ~then_ canBlock ctx stmts + | CValue _, `Var _ -> + failwith "Cannot match value with variable" + | CVar m_acc, `Var v -> + if same_variable ctx m_acc v then + evaluate_stmts ~then_ canBlock ctx stmts + | CVar _, (`Value _ | `Undefined) -> + failwith "Cannot match variable with value") + cases) + l + with INTERNAL_STOP_SWITCH -> () + + and evaluate_when canBlock ctx wdl ed = + let rec aux = function + | (expr, dl, _) :: l -> ( + match evaluate_expr ctx expr with + | Number z when N.(z =. zero ()) -> + evaluate_stmts canBlock ctx (Pos.unmark ed) + | Number _ -> + evaluate_stmts canBlock ctx dl; + aux l + | Undefined -> aux l) + | [] -> () + in + aux wdl + + and evaluate_print ctx std args = + let pctx = Print.fresh std ctx in + List.iter + (fun (arg : Com.Var.t Com.print_arg Pos.marked) -> + match Pos.unmark arg with + | PrintString s -> Print.string pctx s + | PrintAccess (info, m_a) -> ( + match + C.get_access_var ~eval:evaluate_expr pctx.ctx (Pos.unmark m_a) + with + | None -> () + | Some (vsd, var, _) -> + let _, v, _ = C.get_var pctx.ctx None var in + Print.access pctx info vsd v) + | PrintIndent e -> Print.indent pctx (evaluate_expr pctx.ctx e) + | PrintExpr (e, mi, ma) -> + Print.value pctx mi ma (evaluate_expr pctx.ctx e)) + args; + Print.flush pctx + + and evaluate_iterate canBlock ctx var al var_params stmts = + try + List.iter + (fun m_a -> + match C.get_access_var ~eval:evaluate_expr ctx @@ Pos.unmark m_a with + | Some (vsd, v, vorg) -> + C.set_var_ref ctx var vsd v vorg; + evaluate_stmts canBlock ctx stmts + | None -> ()) + al; + List.iter + (fun (vcs, expr, m_sp_opt) -> + let eval vc _ = + StrMap.iter + (fun _ v -> + if + Com.CatVar.compare (Com.Var.cat v) vc = 0 + && not (Com.Var.is_table v) + then ( + let vsd, v, org = C.get_var ctx m_sp_opt v in + C.set_var_ref ctx var vsd v org; + match evaluate_expr ctx expr with + | Number z when N.(z =. one ()) -> + evaluate_stmts canBlock ctx stmts + | _ -> ())) + ctx.ctx_prog.program_vars + in + Com.CatVar.Map.iter eval vcs) + var_params + with + | Stop_instruction (SKId None) -> () + | Stop_instruction (SKId (Some scope)) as exn -> + if scope = Pos.unmark var.name then () else raise exn + + and evaluate_iterate_values canBlock ctx var var_intervals stmts = + try + List.iter + (fun (e0, e1, step) -> + let val0 = evaluate_expr ctx e0 in + let val1 = evaluate_expr ctx e1 in + let valStep = evaluate_expr ctx step in + match (val0, val1, valStep) with + | Number z0, Number z1, Number zStep when not N.(is_zero zStep) -> + let cmp = N.(if zStep > zero () then ( <=. ) else ( >=. )) in + let rec loop i = + if cmp i z1 then ( + let vsd, var, vorg = C.get_var ctx None var in + C.set_var_value_org ctx vsd var vorg (Number i); + evaluate_stmts canBlock ctx stmts; + loop N.(i +. zStep)) + in + loop z0 + | _, _, _ -> ()) + var_intervals + with + | Stop_instruction (SKId None) -> () + | Stop_instruction (SKId (Some scope)) as exn -> + if scope = Pos.unmark var.name then () else raise exn + + and evaluate_stop _ctx scope = raise (Stop_instruction scope) + + and evaluate_restore canBlock ctx al var_params evts evtfs stmts = + let backup backup_vars vsd var vorg = + if Com.Var.is_table var then + let sz = Com.Var.size var in + let rec loop backup_vars i = + if i >= sz then backup_vars + else + let v_i = C.get_var_tab ctx var i in + let value = C.get_var_value_org ctx vsd v_i vorg in + loop ((vsd, v_i, vorg, value) :: backup_vars) (i + 1) + in + loop backup_vars 0 + else + let value = C.get_var_value_org ctx vsd var vorg in + (vsd, var, vorg, value) :: backup_vars + in + let backup_vars = + List.fold_left + (fun backup_vars m_acc -> + match C.get_access_var ~eval:evaluate_expr ctx (Pos.unmark m_acc) with + | Some (vsd, var, vorg) -> backup backup_vars vsd var vorg + | None -> backup_vars) + [] al + in + let backup_vars = + List.fold_left + (fun backup_vars ((var : Com.Var.t), vcs, expr, m_sp_opt) -> + Com.CatVar.Map.fold + (fun vc _ backup_vars -> + StrMap.fold + (fun _ v backup_vars -> + if Com.CatVar.compare (Com.Var.cat v) vc = 0 then ( + let vsd, v', vorg = C.get_var ctx m_sp_opt v in + C.set_var_ref ctx var vsd v' vorg; + match evaluate_expr ctx expr with + | Number z when N.(z =. one ()) -> + backup backup_vars vsd v' vorg + | _ -> backup_vars) + else backup_vars) + ctx.ctx_prog.program_vars backup_vars) + vcs backup_vars) + backup_vars var_params + in + let backup_evts = + List.fold_left + (fun backup_evts expr -> + match evaluate_expr ctx expr with + | Number z -> + let i = Int64.to_int @@ N.to_int z in + let events0 = List.hd ctx.ctx_events in + if 0 <= i && i < Array.length events0 then ( + let evt = events0.(i) in + events0.(i) <- Array.copy evt; + (i, evt) :: backup_evts) + else backup_evts + | _ -> backup_evts) + [] evts + in + let backup_evts = + List.fold_left + (fun backup_evts ((var : Com.Var.t), expr) -> + let events0 = List.hd ctx.ctx_events in + let rec aux backup_evts i = + if i < Array.length events0 then ( + let vi = N.of_int @@ Int64.of_int i in + C.set_var_value ctx None var (Number vi); + match evaluate_expr ctx expr with + | Number z when N.(z =. one ()) -> + let evt = events0.(i) in + events0.(i) <- Array.copy evt; + aux ((i, evt) :: backup_evts) (i + 1) + | _ -> aux backup_evts (i + 1)) + else backup_evts + in + aux backup_evts 0) + backup_evts evtfs + in + let then_ () = + List.iter + (fun (vsd, v, vorg, value) -> C.set_var_value_org ctx vsd v vorg value) + backup_vars; + let events0 = List.hd ctx.ctx_events in + List.iter (fun (i, evt) -> events0.(i) <- evt) backup_evts + in + evaluate_stmts ~then_ canBlock ctx stmts + + and evaluate_arrange_events canBlock ctx sort filter add stmts = + let event_list, nbAdd = + match add with + | Some expr -> ( + match evaluate_expr ctx expr with + | Number z when N.(z >. zero ()) -> + let nb = Int64.to_int @@ N.to_int z in + if nb > 0 then + let nbProgFields = + IntMap.cardinal ctx.ctx_prog.program_event_field_idxs + in + let defEvt = + let init id = + let fname = + IntMap.find id ctx.ctx_prog.program_event_field_idxs + in + let ef = + StrMap.find fname ctx.ctx_prog.program_event_fields + in + match ef.is_var with + | true -> + let defVar = + snd @@ StrMap.min_binding ctx.ctx_prog.program_vars + in + Com.RefVar defVar + | false -> Com.Numeric Undefined + in + Array.init nbProgFields init + in + let init = function 0 -> defEvt | _ -> Array.copy defEvt in + (List.init nb init, nb) + else ([], 0) + | _ -> ([], 0)) + | None -> ([], 0) + in + let events = + match filter with + | Some (var, expr) -> + let events0 = List.hd ctx.ctx_events in + let rec aux res i = + if i >= Array.length events0 then Array.of_list (List.rev res) + else + let vi = Number (N.of_int @@ Int64.of_int i) in + C.set_var_value ctx None var vi; + let res' = + match evaluate_expr ctx expr with + | Number z when N.(z =. one ()) -> events0.(i) :: res + | _ -> res + in + aux res' (i + 1) + in + aux event_list 0 + | None -> + let events0 = List.hd ctx.ctx_events in + let rec aux res i = + if i >= Array.length events0 then Array.of_list (List.rev res) + else aux (events0.(i) :: res) (i + 1) + in + aux event_list 0 + in + ctx.ctx_events <- events :: ctx.ctx_events; + (match sort with + | Some (var0, var1, expr) -> + let sort_fun i _ j _ = + let vi = Number (N.of_int @@ Int64.of_int i) in + C.set_var_value ctx None var0 vi; + let vj = Number (N.of_int @@ Int64.of_int j) in + C.set_var_value ctx None var1 vj; + match evaluate_expr ctx expr with + | Number z when N.(z =. zero ()) -> false + | Number _ -> true + | Undefined -> false + in + Sorting.mergeSort sort_fun nbAdd (Array.length events) events + | None -> ()); + let then_ () = ctx.ctx_events <- List.tl ctx.ctx_events in + evaluate_stmts ~then_ canBlock ctx stmts + + and evaluate_expr (ctx : ctx) (e : Mir.expression Pos.marked) : value = + let out = + try + match Pos.unmark e with + | Com.TestInSet (positive, e0, values) -> + in_set ctx positive (evaluate_expr ctx e0) values + | Comparison (op, e1, e2) -> + let value1 = evaluate_expr ctx e1 in + let value2 = evaluate_expr ctx e2 in + comparison (Pos.unmark op) value1 value2 + | Binop (op, e1, e2) -> + let value1 = evaluate_expr ctx e1 in + let value2 = evaluate_expr ctx e2 in + binop (Pos.unmark op) value1 value2 + | Unop (op, e1) -> unop op @@ evaluate_expr ctx e1 + | Conditional (e1, e2, e3_opt) -> cond ctx e1 e2 e3_opt + | Literal Undefined -> Undefined + | Literal (Float f) -> Number (N.of_float f) + | Var access -> C.get_access_value ~eval:evaluate_expr ctx access + | FuncCall (Pos.Mark (ArrFunc, _), [ arg ]) -> + Funs.arr (evaluate_expr ctx arg) + | FuncCall (Pos.Mark (InfFunc, _), [ arg ]) -> + Funs.inf (evaluate_expr ctx arg) + | FuncCall (Pos.Mark (PresentFunc, _), [ arg ]) -> + Funs.present (evaluate_expr ctx arg) + | FuncCall (Pos.Mark (Supzero, _), [ arg ]) -> + Funs.supzero (evaluate_expr ctx arg) + | FuncCall (Pos.Mark (AbsFunc, _), [ arg ]) -> + Funs.abs (evaluate_expr ctx arg) + | FuncCall (Pos.Mark (MinFunc, _), [ arg1; arg2 ]) -> + Funs.min (evaluate_expr ctx arg1) (evaluate_expr ctx arg2) + | FuncCall (Pos.Mark (MaxFunc, _), [ arg1; arg2 ]) -> + Funs.max (evaluate_expr ctx arg1) (evaluate_expr ctx arg2) + | FuncCall (Pos.Mark (Multimax, _), [ arg1; arg2 ]) -> ( + (* TODO: factorize properly *) + match evaluate_expr ctx arg1 with + | Undefined -> Undefined + | Number f -> ( + let nb = Int64.to_int @@ N.to_int @@ roundf f in + let var_opt = + match Pos.unmark arg2 with + | Var access -> + C.get_access_var ~eval:evaluate_expr ctx access + | _ -> None + in + match var_opt with + | None -> Undefined + | Some (vsd, var, vorg) -> + if Com.Var.is_table var then + let rec loop res i = + if i >= Com.Var.size var || i >= nb then res + else + let var_i = C.get_var_tab ctx var i in + let val_i = C.get_var_value_org ctx vsd var_i vorg in + let res = + match (res, val_i) with + | Undefined, _ -> val_i + | Number _, Undefined -> res + | Number nr, Number ni -> + if N.(nr <. ni) then val_i else res + in + loop res (i + 1) + in + loop Undefined 0 + else if nb >= 1 then C.get_var_value_org ctx vsd var vorg + else Undefined)) + | FuncCall (Pos.Mark (NbEvents, _), _) -> Funs.nb_events ctx + | FuncCall (Pos.Mark (Func fn, _), args) -> + let fd = StrMap.find fn ctx.ctx_prog.program_functions in + evaluate_function ctx fd args + | FuncCall (_, _) -> assert false + | Attribut (m_acc, a) -> get_attr ctx m_acc a + | Size m_acc -> get_size ctx m_acc + | Type (m_acc, m_typ) -> get_type ctx m_acc m_typ + | SameVariable (m_acc0, m_acc1) -> + if same_variable ctx m_acc0 m_acc1 then Number (N.one ()) + else Number (N.zero ()) + | InDomain (m_acc, cvm) -> in_domain ctx m_acc cvm + | NbAnomalies -> Number (N.of_float (float ctx.ctx_nb_anos)) + | NbDiscordances -> Number (N.of_float (float ctx.ctx_nb_discos)) + | NbInformatives -> Number (N.of_float (float ctx.ctx_nb_infos)) + | NbBloquantes -> Number (N.of_float (float ctx.ctx_nb_bloquantes)) + | NbCategory _ | FuncCallLoop _ | Loop _ -> assert false + with + | InternalRuntimeError (e, ctx) -> + if !exit_on_rte then raise_runtime_as_structured e + else raise (InternalRuntimeError (e, ctx)) + | Errors.StructuredError (msg, pos, kont) -> + if !exit_on_rte then + raise + (Errors.StructuredError + ( msg, + pos @ [ (Some "Expression raising the error:", Pos.get e) ], + kont )) + else + raise (InternalRuntimeError (StructuredError (msg, pos, kont), ctx)) + in + if match out with Undefined -> false | Number out -> N.is_nan_or_inf out + then + let e = + NanOrInf + ( (match out with + | Undefined -> assert false + | Number out -> Format.asprintf "%a" N.format_t out), + e ) + in + if !exit_on_rte then raise_runtime_as_structured e + else raise (InternalRuntimeError (e, ctx)) + else out + + and evaluate_stmt (canBlock : bool) (ctx : ctx) (stmt : Mir.m_instruction) : + unit = + match Pos.unmark stmt with + | Com.Affectation (Pos.Mark (assign, _)) -> evaluate_assign ctx assign + | Com.IfThenElse (b, t, f) -> evaluate_ite canBlock ctx b t f + | Com.Switch (c, l) -> evaluate_switch canBlock ctx c l + | Com.WhenDoElse (wdl, ed) -> evaluate_when canBlock ctx wdl ed + | Com.VerifBlock stmts -> evaluate_stmts true ctx stmts + | Com.ComputeTarget (Pos.Mark (tn, _), args, m_sp_opt) -> + let tf = StrMap.find tn ctx.ctx_prog.program_targets in + let vsd = C.get_var_space ctx m_sp_opt in + evaluate_target canBlock ctx tf args vsd + | Com.Print (std, args) -> evaluate_print ctx std args + | Com.Iterate (var, al, var_params, stmts) -> + evaluate_iterate canBlock ctx var al var_params stmts + | Com.Iterate_values (var, var_intervals, stmts) -> + evaluate_iterate_values canBlock ctx var var_intervals stmts + | Com.Stop scope -> evaluate_stop ctx scope + | Com.Restore (al, var_params, evts, evtfs, stmts) -> + evaluate_restore canBlock ctx al var_params evts evtfs stmts + | Com.ArrangeEvents (sort, filter, add, stmts) -> + evaluate_arrange_events canBlock ctx sort filter add stmts + | Com.RaiseError (m_err, var_opt) -> + let is_blocking = + Anomalies.raise ctx (Pos.unmark m_err) (Option.map Pos.unmark var_opt) + in + if is_blocking && ctx.ctx_nb_bloquantes >= 4 && canBlock then + raise BlockingError + | Com.CleanErrors -> Anomalies.clean ctx + | Com.CleanFinalizedErrors -> Anomalies.clean_finalized ctx + | Com.FinalizeErrors -> Anomalies.finalize ~mode_corr:(mode_corr ctx) ctx + | Com.ExportErrors -> Anomalies.export ~mode_corr:(mode_corr ctx) ctx + | Com.ComputeDomain _ | Com.ComputeChaining _ | Com.ComputeVerifs _ -> + assert false + + and evaluate_stmts ?(then_ = ignore) canBlock (ctx : ctx) + (stmts : Mir.m_instruction list) : unit = + let () = + try List.iter (evaluate_stmt canBlock ctx) stmts with + | BlockingError as b_err -> if canBlock then raise b_err + | Stop_instruction _ as exn -> + then_ (); + raise exn + in + then_ () + + and evaluate_function (ctx : ctx) (target : Mir.target) + (args : Mir.m_expression list) : value = + let rec set_args n vl el = + match (vl, el) with + | [], [] -> () + | v :: vl', e :: el' -> + let i = ctx.ctx_tmps_org + n + 1 in + let e_val = evaluate_expr ctx e in + ctx.ctx_tmps.(i).var <- v; + ctx.ctx_tmps.(i).value <- e_val; + set_args (n + 1) vl' el' + | _ -> assert false + in + set_args 0 target.target_args args; + ctx.ctx_tmps.(ctx.ctx_tmps_org).var <- Option.get target.target_result; + ctx.ctx_tmps.(ctx.ctx_tmps_org).value <- Undefined; + evaluate_target_aux ~is_fun:true false ctx target; + ctx.ctx_tmps.(ctx.ctx_tmps_org).value + + and evaluate_target (canBlock : bool) (ctx : ctx) (target : Mir.target) + (args : Mir.m_access list) (vsd : Com.variable_space) : unit = + let rec set_args n vl al = + match (vl, al) with + | v :: vl', m_a :: al' -> ( + ctx.ctx_ref.(ctx.ctx_ref_org + n).var <- v; + match C.get_access_var ~eval:evaluate_expr ctx (Pos.unmark m_a) with + | Some (var_space, ref_var, org) -> + ctx.ctx_ref.(ctx.ctx_ref_org + n).var_space <- var_space; + ctx.ctx_ref.(ctx.ctx_ref_org + n).ref_var <- ref_var; + ctx.ctx_ref.(ctx.ctx_ref_org + n).org <- org; + set_args (n + 1) vl' al' + | None -> ()) + | [], [] -> + let vs_id_sav = ctx.ctx_var_space in + ctx.ctx_var_space <- vsd.vs_id; + evaluate_target_aux ~is_fun:false canBlock ctx target; + ctx.ctx_var_space <- vs_id_sav + | _ -> assert false + in + set_args 0 target.target_args args + + and evaluate_target_aux ~(is_fun : bool) (canBlock : bool) (ctx : ctx) + (target : Mir.target) : unit = + let sav_target = ctx.ctx_target in + ctx.ctx_target <- target; + ctx.ctx_tmps_org <- ctx.ctx_tmps_org + target.target_sz_tmps; + StrMap.iter + (fun _ v -> + let i = ctx.ctx_tmps_org + Com.Var.loc_idx v in + ctx.ctx_tmps.(i).var <- v; + ctx.ctx_tmps.(i).value <- Undefined) + target.target_tmp_vars; + ctx.ctx_ref_org <- ctx.ctx_ref_org + target.target_nb_refs; + let then_ () = + ctx.ctx_ref_org <- ctx.ctx_ref_org - target.target_nb_refs; + ctx.ctx_tmps_org <- ctx.ctx_tmps_org - target.target_sz_tmps + in + let () = + try evaluate_stmts ~then_ canBlock ctx target.target_prog with + | Stop_instruction SKTarget when not is_fun -> () + | Stop_instruction SKFun when is_fun -> () + in + ctx.ctx_target <- sav_target + + let evaluate_program (ctx : ctx) : unit = + try + let main_target = + match + StrMap.find_opt ctx.ctx_prog.program_main_target + ctx.ctx_prog.program_targets + with + | Some t -> t + | None -> + Errors.raise_error "Unable to find main function of Bir program" + in + let vsd = ctx.ctx_prog.program_var_space_def in + ctx.ctx_target <- main_target; + evaluate_target false ctx main_target [] vsd; + evaluate_stmt false ctx (Pos.without Com.ExportErrors) + with + | InternalRuntimeError (e, ctx) -> + if !exit_on_rte then raise_runtime_as_structured e + else raise (InternalRuntimeError (e, ctx)) + | Stop_instruction SKApplication -> + (* The only stop never caught by anything else *) () + | Stop_instruction SKTarget -> (* May not be caught by anything else *) () +end + +module FloatDefInterp = Make (Number.FloatDef) +module FloatMultInterp = Make (Number.FloatMult) +module FloatMfInterp = Make (Number.FloatMf) +module MPFRDefInterp = Make (Number.MPFRDef) +module MPFRMultInterp = Make (Number.MPFRMult) +module MPFRMfInterp = Make (Number.MPFRMf) +module BigIntDefInterp = Make (Number.BigIntDef) +module BigIntMultInterp = Make (Number.BigIntMult) +module BigIntMfInterp = Make (Number.BigIntMf) +module IntvDefInterp = Make (Number.IntvDef) +module IntvMultInterp = Make (Number.IntvMult) +module IntvMfInterp = Make (Number.IntvMf) +module RatDefInterp = Make (Number.RatDef) +module RatMultInterp = Make (Number.RatMult) +module RatMfInterp = Make (Number.RatMf) + +let get_interp (sort : Config.value_sort) (roundops : Config.round_ops) : + (module S) = + match (sort, roundops) with + | RegularFloat, RODefault -> (module FloatDefInterp) + | RegularFloat, ROMulti -> (module FloatMultInterp) + | RegularFloat, ROMainframe _ -> (module FloatMfInterp) + | MPFR _, RODefault -> (module MPFRDefInterp) + | MPFR _, ROMulti -> (module MPFRMultInterp) + | MPFR _, ROMainframe _ -> (module MPFRMfInterp) + | BigInt _, RODefault -> (module BigIntDefInterp) + | BigInt _, ROMulti -> (module BigIntMultInterp) + | BigInt _, ROMainframe _ -> (module BigIntMfInterp) + | Interval, RODefault -> (module IntvDefInterp) + | Interval, ROMulti -> (module IntvMultInterp) + | Interval, ROMainframe _ -> (module IntvMfInterp) + | Rational, RODefault -> (module RatDefInterp) + | Rational, ROMulti -> (module RatMultInterp) + | Rational, ROMainframe _ -> (module RatMfInterp) + +let evaluate_program ~(p : Mir.program) ~(inputs : Com.literal Com.Var.Map.t) + ~(events : (Com.literal, Com.Var.t) Com.event_value StrMap.t list) + ~(sort : Config.value_sort) ~(round_ops : Config.round_ops) : + Com.literal Com.Var.Map.t * Com.Error.Set.t = + Number.setup_precision sort round_ops; + let module Interp = (val get_interp sort round_ops : S) in + let ctx = + let inputs = Com.Var.Map.map Interp.literal_to_value inputs in + let events = + List.map (StrMap.map Interp.literal_event_to_value_event) events + in + Context.empty_ctx ~inputs ~events p + in + let () = + try Interp.evaluate_program ctx + with Interp.InternalRuntimeError (r, _) -> raise (RuntimeError r) + in + Format.pp_print_flush Format.std_formatter (); + Format.pp_print_flush Format.err_formatter (); + let varMap = + let default_space = + ctx.ctx_var_spaces.(ctx.ctx_prog.program_var_space_def.vs_id) + in + let fold _ (var : Com.Var.t) res = + if Com.Var.is_given_back var || true then + let litt = + match Com.Var.cat_var_loc var with + | LocInput -> default_space.input.(Com.Var.loc_idx var) + | LocComputed -> default_space.computed.(Com.Var.loc_idx var) + | LocBase -> default_space.base.(Com.Var.loc_idx var) + in + let fVal = Interp.value_to_literal litt in + Com.Var.Map.add var fVal res + else res + in + StrMap.fold fold ctx.ctx_prog.program_vars Com.Var.Map.empty + in + let anoSet = + let fold res (e, _) = Com.Error.Set.add e res in + List.fold_left fold Com.Error.Set.empty ctx.ctx_exported_anos + in + (varMap, anoSet) + +let evaluate_expr ~(p : Mir.program) ~(e : Mir.expression Pos.marked) + ~(sort : Config.value_sort) ~(round_ops : Config.round_ops) : Com.literal = + let module Interp = (val get_interp sort round_ops : S) in + try + Interp.value_to_literal (Interp.evaluate_expr (Context.empty_ctx p) e) + with + | Stop_instruction _ -> Undefined + | Interp.InternalRuntimeError (r, _) -> raise (RuntimeError r) diff --git a/src/mlang/mir_interpreter/eval.mli b/src/mlang/mir_interpreter/eval.mli new file mode 100644 index 000000000..1e7b46e6e --- /dev/null +++ b/src/mlang/mir_interpreter/eval.mli @@ -0,0 +1,115 @@ +(** Interpretation engine. *) + +val exit_on_rte : bool ref + +(** {2 Generic evaluation functions} *) + +val evaluate_program : + p:M_ir.Mir.program -> + inputs:M_ir.Com.literal M_ir.Com.Var.Map.t -> + events:(M_ir.Com.literal, M_ir.Com.Var.t) M_ir.Com.event_value StrMap.t list -> + sort:Config.value_sort -> + round_ops:Config.round_ops -> + M_ir.Com.literal M_ir.Com.Var.Map.t * M_ir.Com.Error.Set.t +(** Evaluates a whole program and returns the given back variables, as well as + the set of anomalies. The evaluation engine is selected from [sort] and + [roundops]. *) + +val evaluate_expr : + p:M_ir.Mir.program -> + e:M_ir.Mir.expression Pos.marked -> + sort:Config.value_sort -> + round_ops:Config.round_ops -> + M_ir.Com.literal +(** Evaluates a single expression. The evaluation engine is selected from [sort] + and [roundops]. *) + +(** {2 Generic module type} *) + +module type S = sig + type custom_float + + type ctx = custom_float Types.ctx + + exception InternalRuntimeError of Types.run_error * ctx + + (** {2 M Evaluation} *) + + val evaluate_expr : + ctx -> M_ir.Mir.expression Pos.marked -> custom_float Types.value + (** Evaluates an expression. *) + + val evaluate_program : ctx -> unit + (** Evaluates a whole program. Proper initialisation of inputs and events is + required before calling this function (through [update_ctx_with_inputs] + and [update_ctx_with_events]. *) + + (** {2 Helpers} *) + + (** These helpers are here for compatibility with {!module: Context}. *) + + val literal_to_value : M_ir.Com.literal -> custom_float Types.value + + val value_to_literal : custom_float Types.value -> M_ir.Com.literal + + val literal_event_to_value_event : + (M_ir.Com.literal, M_ir.Com.Var.t) M_ir.Com.event_value -> + (custom_float Types.value, M_ir.Com.Var.t) M_ir.Com.event_value +end + +(** {2 Engine builder} *) + +(** Builds an intepretation engine from a number interface + ({!module: M_ir.Mir_number}) and a rounding strategy + ({!module: M_ir.Mir_roundops}). *) +module Make (N : Number.S) : S with type custom_float = N.t + +(** {2 Engines} *) + +(** These modules are instanes of Make with modules defined in + {!module: M_ir.Mir_number} and {!module: M_ir.Mir_roundops}. *) + +module FloatDefInterp : S with type custom_float = float +(** Float with default rounding strategy. *) + +module FloatMultInterp : S with type custom_float = float +(** Float with multithread rounding strategy. *) + +module FloatMfInterp : S with type custom_float = float +(** Float with mainframe rounding strategy. *) + +module MPFRDefInterp : S with type custom_float = Mpfrf.t +(** Multiple-precision floating-point with default rounding strategy. *) + +module MPFRMultInterp : S with type custom_float = Mpfrf.t +(** Multiple-precision floating-point with multithread rounding strategy. *) + +module MPFRMfInterp : S with type custom_float = Mpfrf.t +(** Multiple-precision floating-point with mainframe rounding strategy. *) + +module BigIntDefInterp : S with type custom_float = Mpzf.t +(** Multiple precision integer arithmetic with default rounding strategy. *) + +module BigIntMultInterp : S with type custom_float = Mpzf.t +(** Multiple precision integer arithmetic with multihtread rounding strategy. *) + +module BigIntMfInterp : S with type custom_float = Mpzf.t +(** Multiple precision integer arithmetic with mainframe rounding strategy. *) + +module IntvDefInterp : S with type custom_float = M_ir.Mir_number.interval +(** Multiple-precision floating-point intervals with default rounding strategy. *) + +module IntvMultInterp : S with type custom_float = M_ir.Mir_number.interval +(** Multiple-precision floating-point intervals with multithread rounding strategy. *) + +module IntvMfInterp : S with type custom_float = M_ir.Mir_number.interval +(** Multiple-precision floating-point intervals with mainframe rounding strategy. *) + +module RatDefInterp : S with type custom_float = Mpqf.t +(** Multiple-precision rationals with default rounding strategy. *) + +module RatMultInterp : S with type custom_float = Mpqf.t +(** Multiple-precision rationals with multithread rounding strategy. *) + +module RatMfInterp : S with type custom_float = Mpqf.t +(** Multiple-precision rationals with mainframe rounding strategy. *) diff --git a/src/mlang/mir_interpreter/functions.ml b/src/mlang/mir_interpreter/functions.ml new file mode 100644 index 000000000..fdf5294dc --- /dev/null +++ b/src/mlang/mir_interpreter/functions.ml @@ -0,0 +1,62 @@ +(* TODO: move functions here *) +open Types + +module Make (N : Types.Number) = struct + let false_value () = Number (N.zero ()) + + let true_value () = Number (N.one ()) + + let arr = function + | Number x -> Number (N.roundf x) + | Undefined -> Undefined (*nope:Float 0.*) + + let inf = function + | Number x -> Number (N.truncatef x) + | Undefined -> Undefined + + let present = function Undefined -> false_value () | _ -> true_value () + + let supzero = function + | Undefined -> Undefined + | Number f as n -> if N.compare Com.Lte f (N.zero ()) then Undefined else n + + let abs = function Undefined -> Undefined | Number f -> Number (N.abs f) + + let min i j = + match (i, j) with + | Undefined, Undefined -> Undefined + | Undefined, Number f | Number f, Undefined -> Number (N.min (N.zero ()) f) + | Number fl, Number fr -> Number (N.min fl fr) + + let max i j = + match (i, j) with + | Undefined, Undefined -> Undefined + | Undefined, Number f | Number f, Undefined -> Number (N.max (N.zero ()) f) + | Number fl, Number fr -> Number (N.max fl fr) + + let multimax (i : N.t value) + (j : [ `Table of N.t value list | `Var of N.t value ]) : N.t value = + match (i, j) with + | Undefined, _ -> Undefined + | Number n, _ when N.is_zero n -> Undefined + | Number f, `Table l -> + let nb = Int64.to_int @@ N.to_int @@ N.roundf f in + let rec loop res cpt = function + | [] -> res + | _ when cpt >= nb -> res + | Undefined :: tl -> loop res (cpt + 1) tl + | (Number v as hd) :: tl -> + let res = + match res with + | Undefined -> hd + | Number nr -> if N.(nr <. v) then hd else res + in + loop res (cpt + 1) tl + in + loop Undefined 0 l + | Number _, `Var v -> v + + let nb_events (ctx : 'a ctx) = + let card = Array.length (List.hd ctx.ctx_events) in + Number (N.of_int @@ Int64.of_int @@ card) +end diff --git a/src/mlang/mir_interpreter/functions.mli b/src/mlang/mir_interpreter/functions.mli new file mode 100644 index 000000000..1270c0764 --- /dev/null +++ b/src/mlang/mir_interpreter/functions.mli @@ -0,0 +1,43 @@ +(** Implementation of several function calls as described in + {{:../../../../../fonctions.html}the functions documentation}. + + Note: the interpreter implementation is supposed to be the legitimate + specification. If there are inconsistencies between the documentation + or the C code and the actual behavior of the interprer, the interpreter + is the reference. *) + +module Make (N : Types.Number) : sig + val arr : N.t Types.value -> N.t Types.value + (** Implements the 'arr' call (rounding). *) + + val inf : N.t Types.value -> N.t Types.value + (** Implements the 'inf' call (truncate). *) + + val present : 'a Types.value -> N.t Types.value + (** Implements the 'present' call that checks if the value xis not equal to + undefined. *) + + val supzero : N.t Types.value -> N.t Types.value + (** Implements the 'supzero' call, which returns undefined for strictly negative + values or the argument otherwise. *) + + val abs : N.t Types.value -> N.t Types.value + (** Implements the 'abs' call, calculating the absolute value of its + argument. *) + + val min : N.t Types.value -> N.t Types.value -> N.t Types.value + (** Implements the 'min' call, returning the minimum between two values. *) + + val max : N.t Types.value -> N.t Types.value -> N.t Types.value + (** Implements the 'max' call, returning the maximum between two values. *) + + val multimax : + N.t Types.value -> + [ `Table of N.t Types.value list | `Var of N.t Types.value ] -> + N.t Types.value + (** Implements the 'multimax' call, returning the max value of a subtable. *) + + val nb_events : 'a Types.ctx -> N.t Types.value + (** Implements the 'nb_events' call, returning the number of currently defined + events. *) +end diff --git a/src/mlang/mir_interpreter/number.ml b/src/mlang/mir_interpreter/number.ml new file mode 100644 index 000000000..245797ad8 --- /dev/null +++ b/src/mlang/mir_interpreter/number.ml @@ -0,0 +1,85 @@ +open M_ir + +module BigIntPrecision = struct + let scaling_factor_bits = ref 64 +end + +module MainframeLongSize = struct + let max_long = ref Int64.max_int +end + +module type S = sig + include Mir_number.NumberInterface + + include Mir_roundops.RoundOpsInterface with type t := t +end + +module Make + (N : M_ir.Mir_number.NumberInterface) + (RF : Mir_roundops.RoundOpsFunctor) = +struct + include N + include RF (N) +end + +module FloatDef = + Make (Mir_number.RegularFloatNumber) (Mir_roundops.DefaultRoundOps) +module FloatMult = + Make (Mir_number.RegularFloatNumber) (Mir_roundops.DefaultRoundOps) +module FloatMf = + Make + (Mir_number.RegularFloatNumber) + (Mir_roundops.MainframeRoundOps (MainframeLongSize)) +module MPFRDef = Make (Mir_number.MPFRNumber) (Mir_roundops.DefaultRoundOps) +module MPFRMult = Make (Mir_number.MPFRNumber) (Mir_roundops.MultiRoundOps) +module MPFRMf = + Make + (Mir_number.MPFRNumber) + (Mir_roundops.MainframeRoundOps (MainframeLongSize)) +module BigIntDef = + Make + (Mir_number.BigIntFixedPointNumber + (BigIntPrecision)) + (Mir_roundops.DefaultRoundOps) +module BigIntMult = + Make + (Mir_number.BigIntFixedPointNumber + (BigIntPrecision)) + (Mir_roundops.MultiRoundOps) +module BigIntMf = + Make + (Mir_number.BigIntFixedPointNumber + (BigIntPrecision)) + (Mir_roundops.MainframeRoundOps (MainframeLongSize)) +module IntvDef = Make (Mir_number.IntervalNumber) (Mir_roundops.DefaultRoundOps) +module IntvMult = Make (Mir_number.IntervalNumber) (Mir_roundops.MultiRoundOps) +module IntvMf = + Make + (Mir_number.IntervalNumber) + (Mir_roundops.MainframeRoundOps (MainframeLongSize)) +module RatDef = Make (Mir_number.RationalNumber) (Mir_roundops.DefaultRoundOps) +module RatMult = Make (Mir_number.RationalNumber) (Mir_roundops.MultiRoundOps) +module RatMf = + Make + (Mir_number.RationalNumber) + (Mir_roundops.MainframeRoundOps (MainframeLongSize)) + +let setup_precision (sort : Config.value_sort) (roundops : Config.round_ops) : + unit = + begin + match sort with + | MPFR prec -> Mpfr.set_default_prec prec + | BigInt prec -> BigIntPrecision.scaling_factor_bits := prec + | Interval -> Mpfr.set_default_prec 64 + | _ -> () + end; + match roundops with + | ROMainframe long_size -> + let max_long = + if long_size = 32 then Int64.of_int32 Int32.max_int + else if long_size = 64 then Int64.max_int + else assert false + (* checked when parsing command line *) + in + MainframeLongSize.max_long := max_long + | _ -> () diff --git a/src/mlang/mir_interpreter/number.mli b/src/mlang/mir_interpreter/number.mli new file mode 100644 index 000000000..6372241d6 --- /dev/null +++ b/src/mlang/mir_interpreter/number.mli @@ -0,0 +1,63 @@ +(** Abstraction of value manipulation during the interpretation. *) + +(** This module type merges the {!module M_ir.Mir_number} and + {!module M_ir.Mir_roundops} interface to provide a unique module + for manipulating values. *) +module type S = sig + include M_ir.Mir_number.NumberInterface + + include M_ir.Mir_roundops.RoundOpsInterface with type t := t +end + +module Make + (N : M_ir.Mir_number.NumberInterface) + (RF : M_ir.Mir_roundops.RoundOpsFunctor) : S with type t = N.t + +module FloatDef : S with type t = float +(** Float with default rounding strategy. *) + +module FloatMult : S with type t = float +(** Float with multithread rounding strategy. *) + +module FloatMf : S with type t = float +(** Float with mainframe rounding strategy. *) + +module MPFRDef : S with type t = Mpfrf.t +(** Multiple-precision floating-point with default rounding strategy. *) + +module MPFRMult : S with type t = Mpfrf.t +(** Multiple-precision floating-point with multithread rounding strategy. *) + +module MPFRMf : S with type t = Mpfrf.t +(** Multiple-precision floating-point with mainframe rounding strategy. *) + +module BigIntDef : S with type t = Mpzf.t +(** Multiple-precision floating-point with mainframe rounding strategy. *) + +module BigIntMult : S with type t = Mpzf.t +(** Multiple precision integer arithmetic with multihtread rounding strategy. *) + +module BigIntMf : S with type t = Mpzf.t +(** Multiple precision integer arithmetic with mainframe rounding strategy. *) + +module IntvDef : S with type t = M_ir.Mir_number.interval +(** Multiple-precision floating-point intervals with default rounding strategy. *) + +module IntvMult : S with type t = M_ir.Mir_number.interval +(** Multiple-precision floating-point intervals with multithread rounding strategy. *) + +module IntvMf : S with type t = M_ir.Mir_number.interval +(** Multiple-precision floating-point intervals with mainframe rounding strategy. *) + +module RatDef : S with type t = Mpqf.t +(** Multiple-precision rationals with default rounding strategy. *) + +module RatMult : S with type t = Mpqf.t +(** Multiple-precision rationals with multithread rounding strategy. *) + +module RatMf : S with type t = Mpqf.t +(** Multiple-precision rationals with mainframe rounding strategy. *) + +val setup_precision : Config.value_sort -> Config.round_ops -> unit +(** Initializes the precision and the value sort for the different libraries + used for calculations. *) diff --git a/src/mlang/mir_interpreter/print.ml b/src/mlang/mir_interpreter/print.ml new file mode 100644 index 000000000..1cff30d03 --- /dev/null +++ b/src/mlang/mir_interpreter/print.ml @@ -0,0 +1,73 @@ +open Types + +module Make (N : M_ir.Mir_number.NumberInterface) = struct + let _format_value (fmt : Format.formatter) (x : N.t value) = + match x with + | Undefined -> Com.format_literal fmt Com.Undefined + | Number x -> N.format_t fmt x + + let format_value_prec (mi : int) (ma : int) (fmt : Format.formatter) + (x : N.t value) = + match x with + | Undefined -> Com.format_literal fmt Com.Undefined + | Number x -> N.format_prec_t mi ma fmt x + + let fresh std ctx = + match std with + | Com.StdOut -> + { std; ctx; std_fmt = Format.std_formatter; ctx_pr = ctx.ctx_pr_out } + | Com.StdErr -> + { std; ctx; std_fmt = Format.err_formatter; ctx_pr = ctx.ctx_pr_err } + + let flush (pctx : 'a pctx) = + match pctx.std with + | Com.StdOut -> () + | Com.StdErr -> Format.pp_print_flush pctx.std_fmt () + + let pr_out_indent (pctx : 'a pctx) = + if pctx.ctx_pr.is_newline then ( + for _i = 1 to pctx.ctx_pr.indent do + Format.fprintf pctx.std_fmt " " + done; + pctx.ctx_pr.is_newline <- false) + + let pr_raw (pctx : 'a pctx) s = + let len = String.length s in + let rec aux = function + | n when n >= len -> () + | n -> ( + match s.[n] with + | '\n' -> + Format.fprintf pctx.std_fmt "\n"; + flush pctx; + pctx.ctx_pr.is_newline <- true; + aux (n + 1) + | c -> + pr_out_indent pctx; + Format.fprintf pctx.std_fmt "%c" c; + aux (n + 1)) + in + aux 0 + + let pr_set_indent (pctx : 'a pctx) diff = + pctx.ctx_pr.indent <- max 0 (pctx.ctx_pr.indent + diff) + + let value (pctx : 'a pctx) mi ma value = + pr_raw pctx (Pp.spr "%a" (format_value_prec mi ma) value) + + let string (pctx : 'a pctx) s = + pr_raw pctx s; + flush pctx + + let access (pctx : 'a pctx) pinfo vsd var = + if not vsd.Com.vs_by_default then ( + pr_raw pctx (Pos.unmark vsd.vs_name); + pr_raw pctx "."); + match pinfo with + | Com.Name -> pr_raw pctx (Com.Var.name_str var) + | Com.Alias -> pr_raw pctx (Com.Var.alias_str var) + + and indent (pctx : 'a pctx) = function + | Undefined -> () + | Number diff -> pr_set_indent pctx (Int64.to_int @@ N.to_int diff) +end diff --git a/src/mlang/mir_interpreter/print.mli b/src/mlang/mir_interpreter/print.mli new file mode 100644 index 000000000..32dcbc33e --- /dev/null +++ b/src/mlang/mir_interpreter/print.mli @@ -0,0 +1,26 @@ +module Make (N : M_ir.Mir_number.NumberInterface) : sig + val fresh : M_ir.Com.print_std -> N.t Types.ctx -> N.t Types.pctx + (** Returns a fresh printing context. *) + + val flush : N.t Types.pctx -> unit + (** Flushes the used formatter. *) + + val value : N.t Types.pctx -> int -> int -> N.t Types.value -> unit + (** [value pctx mi ma v] + + Prints [v] with a precision between [mi] and [ma]. *) + + val string : N.t Types.pctx -> string -> unit + (** Prints a string. *) + + val access : + N.t Types.pctx -> + M_ir.Com.print_info -> + M_ir.Com.variable_space -> + M_ir.Com.Var.t -> + unit + (** Prints a variable name/alias within its variable space. *) + + val indent : N.t Types.pctx -> N.t Types.value -> unit + (** Sets a new indentation in the current printing context. *) +end diff --git a/src/mlang/mir_interpreter/types.ml b/src/mlang/mir_interpreter/types.ml new file mode 100644 index 000000000..f9680f5fc --- /dev/null +++ b/src/mlang/mir_interpreter/types.ml @@ -0,0 +1,68 @@ +(* A faire : header *) + +module Com = M_ir.Com + +(** The type values used in the interpreter. *) +type 'f value = Number of 'f | Undefined + +type 'f ctx_tmp_var = { mutable var : Com.Var.t; mutable value : 'f value } +(** An association between a variable and its value. *) + +type ctx_ref_var = { + mutable var : Com.Var.t; + mutable var_space : Com.variable_space; + mutable ref_var : Com.Var.t; + mutable org : int; +} + +type print_ctx = { mutable indent : int; mutable is_newline : bool } + +type 'f ctx_var_space = { + input : 'f Array.t; + computed : 'f Array.t; + base : 'f Array.t; +} + +type 'f ctx = { + ctx_prog : M_ir.Mir.program; + mutable ctx_target : M_ir.Mir.target; + mutable ctx_var_space : int; + ctx_var_spaces : 'f value ctx_var_space Array.t; + ctx_tmps : 'f ctx_tmp_var Array.t; + mutable ctx_tmps_org : int; + ctx_ref : ctx_ref_var Array.t; + mutable ctx_ref_org : int; + ctx_tab_map : Com.Var.t Array.t; + ctx_pr_out : print_ctx; + ctx_pr_err : print_ctx; + mutable ctx_anos : (Com.Error.t * string option) list; + mutable ctx_nb_anos : int; + mutable ctx_nb_discos : int; + mutable ctx_nb_infos : int; + mutable ctx_nb_bloquantes : int; + mutable ctx_archived_anos : StrSet.t; + mutable ctx_finalized_anos : (Com.Error.t * string option) list; + mutable ctx_exported_anos : (Com.Error.t * string option) list; + mutable ctx_events : + ('f value, Com.Var.t) Com.event_value Array.t Array.t list; +} + +type 'f pctx = { + std : Com.print_std; + ctx : 'f ctx; + std_fmt : Format.formatter; + ctx_pr : print_ctx; +} + +type run_error = + | NanOrInf of string * M_ir.Mir.expression Pos.marked + | StructuredError of + (string * (string option * Pos.t) list * (unit -> unit) option) + +exception RuntimeError of run_error + +module type Number = sig + include M_ir.Mir_number.NumberInterface + + include M_ir.Mir_roundops.RoundOpsInterface with type t := t +end diff --git a/src/mlang/test_framework/dune b/src/mlang/test_framework/dune index ba5d23f0a..a9258fea0 100644 --- a/src/mlang/test_framework/dune +++ b/src/mlang/test_framework/dune @@ -9,7 +9,7 @@ (public_name mlang.irj_utils) (flags (:standard -open Utils -open M_ir)) - (libraries m_frontend m_ir utils menhirLib parmap str)) + (libraries m_frontend m_ir m_interpreter utils menhirLib parmap str)) ;; This section deals with the .messages file. diff --git a/src/mlang/test_framework/test_interpreter.ml b/src/mlang/test_framework/test_interpreter.ml index a5e61b22b..b8015ba28 100644 --- a/src/mlang/test_framework/test_interpreter.ml +++ b/src/mlang/test_framework/test_interpreter.ml @@ -196,8 +196,8 @@ let check_test (program : Mir.program) (test_name : string) (* Cli.debug_print "Combined Program (w/o verif conds):@.%a@." Format_bir.format_program program; *) let varMap, anoSet = - Mir_interpreter.evaluate_program program inst.vars inst.events - value_sort round_ops + M_interpreter.Eval.evaluate_program ~p:program ~inputs:inst.vars + ~events:inst.events ~sort:value_sort ~round_ops in let nbErrs = check_vars inst.expectedVars varMap @@ -238,7 +238,7 @@ let check_all_tests (p : Mir.program) (test_dir : string) |> List.sort String.compare |> Array.of_list in let ign_vars = ignored_vars_set p ignored_vars_list in - Mir_interpreter.exit_on_rte := false; + M_interpreter.Eval.exit_on_rte := false; let dbg_warning = !Config.warning_flag in let dbg_time = !Config.display_time in Config.warning_flag := false; @@ -246,9 +246,6 @@ let check_all_tests (p : Mir.program) (test_dir : string) (* let _, finish = Config.create_progress_bar "Testing files" in*) let process (name : string) ((successes, failures) : process_acc) : process_acc = - let module Interp = (val Mir_interpreter.get_interp value_sort round_ops - : Mir_interpreter.S) - in try Config.debug_flag := false; check_test p (test_dir ^ name) value_sort round_ops ign_vars; @@ -264,14 +261,14 @@ let check_all_tests (p : Mir.program) (test_dir : string) Errors.format_structured_error (msg, pos); (match kont with None -> () | Some kont -> kont ()); (successes, failures) - | Interp.RuntimeError (run_error, _) -> ( + | M_interpreter.Types.RuntimeError run_error -> ( match run_error with - | Interp.StructuredError (msg, pos, kont) -> + | StructuredError (msg, pos, kont) -> Cli.error_print "Error in test %s: %a" name Errors.format_structured_error (msg, pos); (match kont with None -> () | Some kont -> kont ()); (successes, failures) - | Interp.NanOrInf (msg, Pos.Mark (_, pos)) -> + | NanOrInf (msg, Pos.Mark (_, pos)) -> Cli.error_print "Runtime error in test %s: NanOrInf (%s, %a)" name msg Pos.format pos; (successes, failures)) @@ -301,7 +298,7 @@ let check_all_tests (p : Mir.program) (test_dir : string) let check_one_test (p : Mir.program) (name : string) (value_sort : Config.value_sort) (round_ops : Config.round_ops) = let ign_vars = ignored_vars_set p ignored_vars_list in - Mir_interpreter.exit_on_rte := false; + M_interpreter.Eval.exit_on_rte := false; (* sort by increasing size, hoping that small files = simple tests *) let dbg_warning = !Config.warning_flag in let dbg_time = !Config.display_time in @@ -309,9 +306,6 @@ let check_one_test (p : Mir.program) (name : string) Config.display_time := false; (* let _, finish = Config.create_progress_bar "Testing files" in*) let is_ok = - let module Interp = (val Mir_interpreter.get_interp value_sort round_ops - : Mir_interpreter.S) - in try Config.debug_flag := false; check_test p name value_sort round_ops ign_vars; @@ -325,14 +319,14 @@ let check_one_test (p : Mir.program) (name : string) Errors.format_structured_error (msg, pos); (match kont with None -> () | Some kont -> kont ()); Some 0 - | Interp.RuntimeError (run_error, _) -> ( + | M_interpreter.Types.RuntimeError run_error -> ( match run_error with - | Interp.StructuredError (msg, pos, kont) -> + | StructuredError (msg, pos, kont) -> Cli.error_print "Error in test %s: %a" name Errors.format_structured_error (msg, pos); (match kont with None -> () | Some kont -> kont ()); Some 0 - | Interp.NanOrInf (msg, Pos.Mark (_, pos)) -> + | NanOrInf (msg, Pos.Mark (_, pos)) -> Cli.error_print "Runtime error in test %s: NanOrInf (%s, %a)" name msg Pos.format pos; Some 0)