From 56eef574fea5ba8c6e893281ffe850b94f7ffd2b Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 22 Jan 2026 10:43:14 +0100 Subject: [PATCH 1/2] =?UTF-8?q?Verification=20de=20l'utilisation=20des=20v?= =?UTF-8?q?ariables=20temporaires=20et=20arguments=20en=20tant=20que=20r?= =?UTF-8?q?=C3=A9f=C3=A9rence?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/mlang/m_frontend/validator.ml | 40 ++++++++++++++++++++++++++++--- src/mlang/m_ir/com.ml | 5 ++++ src/mlang/m_ir/com.mli | 2 ++ 3 files changed, 44 insertions(+), 3 deletions(-) diff --git a/src/mlang/m_frontend/validator.ml b/src/mlang/m_frontend/validator.ml index 46ab0b702..7e5488334 100644 --- a/src/mlang/m_frontend/validator.ml +++ b/src/mlang/m_frontend/validator.ml @@ -462,6 +462,16 @@ module Err = struct case in Errors.raise_spanned_error msg pos + + let unexpected_variable_scope ~var_scope ~expected_scope (Pos.Mark (v, pos)) = + let varname = Com.get_var_name v in + let msg = + Pp.spr + "Variable %s is a %a variable, which should be a %s variable in this \ + context" + varname Com.format_simple_scope var_scope expected_scope + in + Errors.raise_spanned_error msg pos end type syms = Com.DomainId.t Pos.marked Com.DomainIdMap.t @@ -1515,8 +1525,29 @@ let check_var_space (m_sp_opt : Com.var_space) (env : var_env) : unit = | Some _ -> () | None -> Err.unknown_var_space sp_name (Pos.get m_sp))) -let check_variable (m_sp_opt : Com.var_space) (m_vn : Com.m_var_name) - (idx_mem : var_mem_type) (env : var_env) : unit = +let check_right_scope ~env ~must_be (Pos.Mark (var, _) as m_vn) = + let v_name = Com.get_normal_var var in + let var = + let id = StrMap.find v_name env.vars in + IntMap.find id env.prog.prog_dict + in + match must_be with + | `Tgv when Com.Var.is_tgv var -> () + | `Ref when Com.Var.is_ref var -> () + | `Temp when Com.Var.is_temp var -> () + | `Tgv -> + Err.unexpected_variable_scope m_vn ~var_scope:var.scope + ~expected_scope:"TGV" + | `Ref -> + Err.unexpected_variable_scope m_vn ~var_scope:var.scope + ~expected_scope:"reference" + | `Temp -> + Err.unexpected_variable_scope m_vn ~var_scope:var.scope + ~expected_scope:"temp" + +let check_variable ?(must_be : [ `Tgv | `Ref | `Temp ] option) + (m_sp_opt : Com.var_space) (m_vn : Com.m_var_name) (idx_mem : var_mem_type) + (env : var_env) : unit = let decl_mem, decl_pos = Pos.to_couple @@ get_var_mem_type m_vn env in (match (decl_mem, idx_mem) with | _, Both | Num, Num | Table, Table -> () @@ -1525,6 +1556,9 @@ let check_variable (m_sp_opt : Com.var_space) (m_vn : Com.m_var_name) | Both, Table -> Err.mixed_variable_used_as_table decl_pos (Pos.get m_vn)*) | Num, Table -> Err.variable_used_as_table decl_pos (Pos.get m_vn) | Table, Num -> Err.table_used_as_variable decl_pos (Pos.get m_vn)); + (match must_be with + | None -> () + | Some must_be -> check_right_scope ~env ~must_be m_vn); match m_sp_opt with | None -> () | Some (m_sp, _) -> @@ -1729,7 +1763,7 @@ let rec check_instructions (env : var_env) | Some _ -> Err.event_field_is_not_a_reference f_name f_pos | None -> Err.unknown_event_field f_name f_pos); let m_i' = map_expr env m_i in - check_variable None m_v Num env; + check_variable ~must_be:`Tgv None m_v Num env; let m_v' = map_var env m_v in let f' = Com.SingleFormula (EventFieldRef (m_i', f, iFmt, m_v')) diff --git a/src/mlang/m_ir/com.ml b/src/mlang/m_ir/com.ml index 0edbbbb46..f97061ccf 100644 --- a/src/mlang/m_ir/com.ml +++ b/src/mlang/m_ir/com.ml @@ -1572,3 +1572,8 @@ let rec format_instruction form_var form_err = and format_instructions form_var form_err fmt instrs = Pp.list "" (Pp.unmark (format_instruction form_var form_err)) fmt instrs + +let format_simple_scope ppf = function + | Var.Tgv _ -> Pp.string ppf "TGV" + | Var.Temp _ -> Pp.string ppf "temp" + | Ref -> Pp.string ppf "Ref" diff --git a/src/mlang/m_ir/com.mli b/src/mlang/m_ir/com.mli index 3e4b4a971..3afb61b71 100644 --- a/src/mlang/m_ir/com.mli +++ b/src/mlang/m_ir/com.mli @@ -685,3 +685,5 @@ val format_instructions : Pp.t -> ('v, 'e) m_instruction list -> unit + +val format_simple_scope : Pp.t -> Var.scope -> unit From 34ebbd84d7a9d7f17488d832c2b4180c8fda0a71 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 23 Jan 2026 14:22:20 +0100 Subject: [PATCH 2/2] =?UTF-8?q?Les=20references=20dans=20champ=5Fevenent?= =?UTF-8?q?=20peuvent=20=C3=AAtre=20des=20ref?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/mlang/m_frontend/validator.ml | 52 +++++++++++++++---------------- src/mlang/m_ir/mir.mli | 16 +++++----- 2 files changed, 32 insertions(+), 36 deletions(-) diff --git a/src/mlang/m_frontend/validator.ml b/src/mlang/m_frontend/validator.ml index 7e5488334..3003c8ed2 100644 --- a/src/mlang/m_frontend/validator.ml +++ b/src/mlang/m_frontend/validator.ml @@ -1525,29 +1525,8 @@ let check_var_space (m_sp_opt : Com.var_space) (env : var_env) : unit = | Some _ -> () | None -> Err.unknown_var_space sp_name (Pos.get m_sp))) -let check_right_scope ~env ~must_be (Pos.Mark (var, _) as m_vn) = - let v_name = Com.get_normal_var var in - let var = - let id = StrMap.find v_name env.vars in - IntMap.find id env.prog.prog_dict - in - match must_be with - | `Tgv when Com.Var.is_tgv var -> () - | `Ref when Com.Var.is_ref var -> () - | `Temp when Com.Var.is_temp var -> () - | `Tgv -> - Err.unexpected_variable_scope m_vn ~var_scope:var.scope - ~expected_scope:"TGV" - | `Ref -> - Err.unexpected_variable_scope m_vn ~var_scope:var.scope - ~expected_scope:"reference" - | `Temp -> - Err.unexpected_variable_scope m_vn ~var_scope:var.scope - ~expected_scope:"temp" - -let check_variable ?(must_be : [ `Tgv | `Ref | `Temp ] option) - (m_sp_opt : Com.var_space) (m_vn : Com.m_var_name) (idx_mem : var_mem_type) - (env : var_env) : unit = +let check_variable (m_sp_opt : Com.var_space) (m_vn : Com.m_var_name) + (idx_mem : var_mem_type) (env : var_env) : unit = let decl_mem, decl_pos = Pos.to_couple @@ get_var_mem_type m_vn env in (match (decl_mem, idx_mem) with | _, Both | Num, Num | Table, Table -> () @@ -1556,9 +1535,6 @@ let check_variable ?(must_be : [ `Tgv | `Ref | `Temp ] option) | Both, Table -> Err.mixed_variable_used_as_table decl_pos (Pos.get m_vn)*) | Num, Table -> Err.variable_used_as_table decl_pos (Pos.get m_vn) | Table, Num -> Err.table_used_as_variable decl_pos (Pos.get m_vn)); - (match must_be with - | None -> () - | Some must_be -> check_right_scope ~env ~must_be m_vn); match m_sp_opt with | None -> () | Some (m_sp, _) -> @@ -1577,6 +1553,27 @@ let check_variable ?(must_be : [ `Tgv | `Ref | `Temp ] option) else if Com.Var.is_temp var then Err.tmp_var_has_no_var_space v_name (Pos.get m_vn) +let check_variable_can_be_referenced + (Pos.Mark (v_name, pos) as m_v : Com.m_var_name) (env : var_env) : unit = + let v_name = Com.get_normal_var v_name in + let var = + let id = StrMap.find v_name env.vars in + IntMap.find id env.prog.prog_dict + in + match var.scope with + | Tgv _ -> () + | Ref -> + Errors.print_spanned_warning + (Format.sprintf + "Variable %s used to set an event reference. Make sure it is not a \ + temporary variable, otherwise this instruction will have no \ + effect." + v_name) + pos + | Temp _ -> + Err.unexpected_variable_scope ~var_scope:var.scope ~expected_scope:"Tgv" + m_v + let check_expression (env : var_env) (m_expr : Mast.m_expression) : unit = let get_var m_v = Pos.same (Com.get_normal_var @@ Pos.unmark m_v) m_v in let fold_sp m_sp_opt env _acc = check_var_space m_sp_opt env in @@ -1763,7 +1760,8 @@ let rec check_instructions (env : var_env) | Some _ -> Err.event_field_is_not_a_reference f_name f_pos | None -> Err.unknown_event_field f_name f_pos); let m_i' = map_expr env m_i in - check_variable ~must_be:`Tgv None m_v Num env; + check_variable None m_v Num env; + check_variable_can_be_referenced m_v env; let m_v' = map_var env m_v in let f' = Com.SingleFormula (EventFieldRef (m_i', f, iFmt, m_v')) 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;