From 6883156be0f16f361f28c97adcdb7097327d9ff2 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 10 Mar 2026 10:09:18 +0000 Subject: [PATCH 1/3] Initial plan From 54c72de11f07b0425e698f5ea63f0a80024df213 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 10 Mar 2026 10:31:17 +0000 Subject: [PATCH 2/3] Fix FIXME comments: remove unused parameters and improve error messages Co-authored-by: namasikanam <22532925+namasikanam@users.noreply.github.com> --- src/ecCoreGoal.ml | 13 +++++-------- src/ecCoreGoal.mli | 8 ++++---- src/ecHiGoal.ml | 2 +- src/ecIo.ml | 2 +- src/ecLowGoal.ml | 6 +++--- src/ecLowGoal.mli | 2 +- src/ecPrinting.ml | 2 +- src/ecScope.ml | 3 ++- src/ecUnify.ml | 2 -- src/ecUnify.mli | 3 +-- src/phl/ecPhlInline.ml | 15 +++++++++------ src/phl/ecPhlSkip.ml | 8 ++++---- src/phl/ecPhlUpto.ml | 16 ++++++++-------- 13 files changed, 40 insertions(+), 42 deletions(-) diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 4b75e5b0c1..6bc97e1fc2 100644 --- a/src/ecCoreGoal.ml +++ b/src/ecCoreGoal.ml @@ -207,11 +207,10 @@ let mk_tcerror ?(catchable = true) ?penv ?loc msg = exception TcError of tcerror (* -------------------------------------------------------------------- *) -let tc_error (penv : proofenv) ?(catchable = true) ?loc ?who fmt = +let tc_error (penv : proofenv) ?(catchable = true) ?loc fmt = let buf = Buffer.create 127 in let fbuf = Format.formatter_of_buffer buf in let loc = loc |> omap (fun loc -> mk_location loc) in - ignore (who : string option); (* FIXME: remove? *) Format.kfprintf (fun _ -> Format.pp_print_flush fbuf (); @@ -221,8 +220,7 @@ let tc_error (penv : proofenv) ?(catchable = true) ?loc ?who fmt = fbuf fmt (* -------------------------------------------------------------------- *) -let tc_error_exn (penv : proofenv) ?(catchable = true) ?loc ?who exn = - ignore (who : string option); +let tc_error_exn (penv : proofenv) ?(catchable = true) ?loc exn = raise (TcError ( { tc_catchable = catchable; tc_proofenv = Some penv; @@ -251,7 +249,7 @@ let tacuerror_exn ?(catchable = true) exn = tc_reloced = None; }) (* -------------------------------------------------------------------- *) -let tc_error_lazy (penv : proofenv) ?(catchable = true) ?loc ?who msg = +let tc_error_lazy (penv : proofenv) ?(catchable = true) ?loc msg = let getmsg () = let buf = Buffer.create 127 in let fbuf = Format.formatter_of_buffer buf in @@ -261,13 +259,12 @@ let tc_error_lazy (penv : proofenv) ?(catchable = true) ?loc ?who msg = let loc = loc |> omap (fun loc -> mk_location loc) in - ignore (who : string option); (* FIXME: remove? *) raise (TcError (mk_tcerror ~catchable ~penv ?loc (lazy (getmsg ())))) (* -------------------------------------------------------------------- *) type symkind = [`Lemma | `Operator | `Local] -let tc_lookup_error pe ?loc ?who kind qs = +let tc_lookup_error pe ?loc kind qs = let string_of_kind kind = match kind with | `Lemma -> "lemma" @@ -275,7 +272,7 @@ let tc_lookup_error pe ?loc ?who kind qs = | `Local -> "local variable" in - tc_error_lazy pe ~catchable:true ?loc ?who + tc_error_lazy pe ~catchable:true ?loc (fun fmt -> Format.fprintf fmt "unknown %s `%s'" (string_of_kind kind) diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli index f574b49bf3..2fdc846435 100644 --- a/src/ecCoreGoal.mli +++ b/src/ecCoreGoal.mli @@ -207,15 +207,15 @@ val closed : proof -> bool (* -------------------------------------------------------------------- *) val tc_error : - proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string + proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a val tc_error_exn : - proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string + proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> exn -> 'a val tc_error_lazy : - proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string + proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> (Format.formatter -> unit) -> 'a (* -------------------------------------------------------------------- *) @@ -229,7 +229,7 @@ val tacuerror_exn : type symkind = [`Lemma | `Operator | `Local] val tc_lookup_error : - proofenv -> ?loc:EcLocation.t -> ?who:string -> symkind -> qsymbol -> 'a + proofenv -> ?loc:EcLocation.t -> symkind -> qsymbol -> 'a (* -------------------------------------------------------------------- *) val reloc : EcLocation.t -> ('a -> 'b) -> 'a -> 'b diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index d34ba4aa76..59e2430860 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -1205,7 +1205,7 @@ let process_view1 pe tc = FApi.t_internal (FApi.t_seqsub (EcLowGoal.t_cut cutf) - [EcLowGoal.t_close ~who:"view" discharge; + [EcLowGoal.t_close discharge; EcLowGoal.t_clear top]) tc diff --git a/src/ecIo.ml b/src/ecIo.ml index 016545d85c..b90bc40856 100644 --- a/src/ecIo.ml +++ b/src/ecIo.ml @@ -198,7 +198,7 @@ let parseall (ecreader : ecreader) = | EcParsetree.P_DocComment _ -> aux acc | EcParsetree.P_Undo _ | EcParsetree.P_Exit -> - assert false (* FIXME *) + raise (EcParsetree.ParseError (EcLocation.dummy, Some "unexpected undo/exit command")) in aux [] diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 6aac3f5730..a11cc460c4 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -280,14 +280,14 @@ let t_admit (tc : tcenv1) = (* -------------------------------------------------------------------- *) let t_fail (tc : tcenv1) = - tc_error !!tc ~who:"fail" "explicit call to [fail]" + tc_error !!tc "explicit call to [fail]" (* -------------------------------------------------------------------- *) -let t_close ?who (t : FApi.backward) (tc : tcenv1) = +let t_close (t : FApi.backward) (tc : tcenv1) = let tc = t tc in if not (FApi.tc_done tc) then - tc_error !$tc ?who "expecting a closed goal"; + tc_error !$tc "expecting a closed goal"; tc (* -------------------------------------------------------------------- *) diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index ef5dca0989..abe0c6ee7d 100644 --- a/src/ecLowGoal.mli +++ b/src/ecLowGoal.mli @@ -32,7 +32,7 @@ val t_admit : FApi.backward val t_true : FApi.backward val t_fail : FApi.backward val t_id : FApi.backward -val t_close : ?who:string -> FApi.backward -> FApi.backward +val t_close : FApi.backward -> FApi.backward val t_shuffle : EcIdent.t list -> FApi.backward (* -------------------------------------------------------------------- *) diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 30dd941ba3..625e9811c0 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -245,7 +245,7 @@ module PPEnv = struct fun sm -> check_for_local sm; let ue = EcUnify.UniEnv.create None in - match EcUnify.select_op ~hidden:true ~filter tvi ppe.ppe_env sm ue dom with + match EcUnify.select_op ~filter tvi ppe.ppe_env sm ue dom with | [(p1, _), _, _, _] -> p1 | _ -> raise (EcEnv.LookupFailure (`QSymbol sm)) in diff --git a/src/ecScope.ml b/src/ecScope.ml index e7a753b0fe..eca2761a4c 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -2659,7 +2659,8 @@ module Ty = struct | _ -> if EcUtils.is_some tci.pti_args then hierror "unsupported-option"; - failwith "unsupported" (* FIXME *) + hierror "unsupported instance: %s" + (EcSymbols.string_of_qsymbol (EcLocation.unloc tci.pti_name)) end (* -------------------------------------------------------------------- *)module Search = struct diff --git a/src/ecUnify.ml b/src/ecUnify.ml index 45cc667535..1226c38159 100644 --- a/src/ecUnify.ml +++ b/src/ecUnify.ml @@ -332,7 +332,6 @@ type select_result = (EcPath.path * ty list) * ty * unienv * sbody option (* -------------------------------------------------------------------- *) let select_op - ?(hidden : bool = false) ?(filter : EcPath.path -> operator -> bool = fun _ _ -> true) (tvi : tvar_inst option) (env : EcEnv.env) @@ -341,7 +340,6 @@ let select_op (sig_ : ty list * ty option) : select_result list = - ignore hidden; (* FIXME *) let module D = EcDecl in diff --git a/src/ecUnify.mli b/src/ecUnify.mli index d19596eb6b..60578dbb04 100644 --- a/src/ecUnify.mli +++ b/src/ecUnify.mli @@ -43,8 +43,7 @@ type sbody = ((EcIdent.t * ty) list * expr) Lazy.t type select_result = (EcPath.path * ty list) * ty * unienv * sbody option val select_op : - ?hidden:bool - -> ?filter:(path -> operator -> bool) + ?filter:(path -> operator -> bool) -> tvi -> EcEnv.env -> qsymbol diff --git a/src/phl/ecPhlInline.ml b/src/phl/ecPhlInline.ml index 8dca495ffe..a0ae141d37 100644 --- a/src/phl/ecPhlInline.ml +++ b/src/phl/ecPhlInline.ml @@ -151,7 +151,7 @@ module LowInternal = struct me (List.combine sps bs) in me, [i_match (e, bs)] - | _, _ -> assert false (* FIXME error message *) + | _, _ -> tc_error !!tc "code pattern doesn't match instruction type" and inline_s me sp s = match sp with @@ -259,7 +259,7 @@ module HiInternal = struct aux_s 0 s.s_node (* ------------------------------------------------------------------ *) - let pat_of_occs cond occs s = + let pat_of_occs tc cond occs s = let occs = ref occs in let rec aux_i occ i = @@ -298,7 +298,10 @@ module HiInternal = struct let sp = snd (aux_s 0 0 s.s_node) in - assert (Sint.is_empty !occs); sp (* FIXME error message *) + if not (Sint.is_empty !occs) then + tc_error !!tc "invalid occurrence(s): %s" + (String.concat ", " (List.map string_of_int (Sint.elements !occs))); + sp (* ------------------------------------------------------------------ *) let pat_of_spath = @@ -390,15 +393,15 @@ let process_inline_occs ~use_tuple side cond occs tc = match concl.f_node, side with | FequivS es, Some b -> let st = sideif b es.es_sl es.es_sr in - let sp = HiInternal.pat_of_occs cond occs st in + let sp = HiInternal.pat_of_occs tc cond occs st in t_inline_equiv ~use_tuple b sp tc | FhoareS hs, None -> - let sp = HiInternal.pat_of_occs cond occs hs.hs_s in + let sp = HiInternal.pat_of_occs tc cond occs hs.hs_s in t_inline_hoare ~use_tuple sp tc | FbdHoareS bhs, None -> - let sp = HiInternal.pat_of_occs cond occs bhs.bhs_s in + let sp = HiInternal.pat_of_occs tc cond occs bhs.bhs_s in t_inline_bdhoare ~use_tuple sp tc | _, _ -> tc_error !!tc "invalid arguments" diff --git a/src/phl/ecPhlSkip.ml b/src/phl/ecPhlSkip.ml index db7c40e37f..102ca1d1e9 100644 --- a/src/phl/ecPhlSkip.ml +++ b/src/phl/ecPhlSkip.ml @@ -43,9 +43,9 @@ module LowInternal = struct let bhs = tc1_as_bdhoareS tc in if not (List.is_empty bhs.bhs_s.s_node) then - tc_error !!tc ~who:"skip" "instruction list is not empty"; + tc_error !!tc "instruction list is not empty"; if bhs.bhs_cmp <> FHeq && bhs.bhs_cmp <> FHge then - tc_error !!tc ~who:"skip" ""; + tc_error !!tc ""; let concl = map_ss_inv2 f_imp (bhs_pr bhs) (bhs_po bhs) in let concl = EcSubst.f_forall_mems_ss_inv bhs.bhs_m concl in @@ -75,9 +75,9 @@ module LowInternal = struct let es = tc1_as_equivS tc in if not (List.is_empty es.es_sl.s_node) then - tc_error !!tc ~who:"skip" "left instruction list is not empty"; + tc_error !!tc "left instruction list is not empty"; if not (List.is_empty es.es_sr.s_node) then - tc_error !!tc ~who:"skip" "right instruction list is not empty"; + tc_error !!tc "right instruction list is not empty"; let concl = map_ts_inv2 f_imp (es_pr es) (es_po es) in let concl = EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr concl in diff --git a/src/phl/ecPhlUpto.ml b/src/phl/ecPhlUpto.ml index 6711e4889e..9e6b6f7c28 100644 --- a/src/phl/ecPhlUpto.ml +++ b/src/phl/ecPhlUpto.ml @@ -223,28 +223,28 @@ let t_uptobad_r tc = let pr1, pr2 = try t2_map destr_pr (destr_eq concl) with DestrError _ -> - tc_error !!tc ~who:"byupto" "expecting a formula of the form \"Pr[_] = Pr[_]\"" + tc_error !!tc "expecting a formula of the form \"Pr[_] = Pr[_]\"" in if not (EcMemory.mem_equal pr1.pr_mem pr2.pr_mem) then - tc_error !!tc ~who:"byupto" "the initial memories should be equal"; + tc_error !!tc "the initial memories should be equal"; if not (is_conv ~ri:full_red hyps pr1.pr_args pr2.pr_args) then - tc_error !!tc ~who:"byupto" "the initial arguments should be equal"; + tc_error !!tc "the initial arguments should be equal"; if not (ss_inv_alpha_eq hyps pr1.pr_event pr2.pr_event) then - tc_error !!tc ~who:"byupto" "the events should be equal"; + tc_error !!tc "the events should be equal"; let bad = try destr_event (pr1.pr_event) with DestrError _ -> - tc_error !!tc ~who:"byupto" "the event should have the form \"E /\ !bad\" or \"!bad\"" + tc_error !!tc "the event should have the form \"E /\\ !bad\" or \"!bad\"" in begin match f_upto_init env bad pr1.pr_fun pr2.pr_fun with - | false -> tc_error !!tc ~who:"byupto" "the two functions are not equal upto bad" + | false -> tc_error !!tc "the two functions are not equal upto bad" | true -> () | exception BadAssign (f, i) -> let ppenv = EcPrinting.PPEnv.ofenv env in let pp_fun fmt = function | None -> () | Some f -> Format.fprintf fmt " in function %a" (EcPrinting.pp_funname ppenv) f in - tc_error !!tc ~who:"byupto" "bad is assigned after being set to true%a, %a" + tc_error !!tc "bad is assigned after being set to true%a, %a" pp_fun f (EcPrinting.pp_instr ppenv) i end; FApi.xmutate1 tc `HlUpto [] @@ -422,4 +422,4 @@ let process_uptobad tc = "expecting a goal of the form \"Pr[_] <= Pr[_] + Pr[_]\" or \"`|Pr[_] - Pr[_]| <= _\"" end | _ -> - tc_error !!tc ~who:"byupto" "expecting a goal of the form \" _ <= _\"" + tc_error !!tc "expecting a goal of the form \" _ <= _\"" From 04e63b5e893e84db222e2e0aabd75951df71f172 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 10 Mar 2026 10:42:57 +0000 Subject: [PATCH 3/3] Fix additional FIXME comments: improve error handling and handle missing cases Co-authored-by: namasikanam <22532925+namasikanam@users.noreply.github.com> --- src/ecEnv.ml | 13 +++++++++---- src/ecPV.ml | 13 +++++++------ src/ecProofTerm.ml | 2 +- src/ecTyping.ml | 2 +- src/phl/ecPhlFel.ml | 4 +++- src/phl/ecPhlSkip.ml | 2 +- 6 files changed, 22 insertions(+), 14 deletions(-) diff --git a/src/ecEnv.ml b/src/ecEnv.ml index edd45ca71f..2312c7190e 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -1685,8 +1685,8 @@ module Fun = struct let actmem_body me fun_ = match fun_.f_def with - | FBabs _ -> assert false (* FIXME error message *) - | FBalias _ -> assert false (* FIXME error message *) + | FBabs _ -> invalid_arg "actmem_body: function has no concrete body (abstract)" + | FBalias _ -> invalid_arg "actmem_body: function has no concrete body (alias)" | FBdef fd -> let mem = EcMemory.empty_local ~witharg:false me in let mem = add_params mem fun_ in @@ -3337,8 +3337,13 @@ module LDecl = struct | LD_hyp f -> LD_hyp (Fsubst.f_subst s f) - | LD_abs_st _ -> (* FIXME *) - assert false + | LD_abs_st us -> + let subst_pv_ty (pv, ty) = (pv_subst s pv, ty_subst s ty) in + LD_abs_st { + aus_calls = List.map (x_subst s) us.aus_calls; + aus_reads = List.map subst_pv_ty us.aus_reads; + aus_writes = List.map subst_pv_ty us.aus_writes; + } (* ------------------------------------------------------------------ *) let ld_fv = function diff --git a/src/ecPV.ml b/src/ecPV.ml index c1c297d754..e7c5beb779 100644 --- a/src/ecPV.ml +++ b/src/ecPV.ml @@ -657,12 +657,13 @@ module Mpv2 = struct let add_glob env mp1 mp2 eqs = let mp1, mp2 = NormMp.norm_mpath env mp1, NormMp.norm_mpath env mp2 in - (* FIXME error message *) - if not (EcPath.m_equal mp1 mp2) then assert false; - if not (mp1.m_args = []) then assert false; + if not (EcPath.m_equal mp1 mp2) then + invalid_arg "add_glob: module paths are not equal"; + if not (mp1.m_args = []) then + invalid_arg "add_glob: module path has functor arguments"; begin match mp1.m_top with | `Local _ -> () - | _ -> assert false + | _ -> invalid_arg "add_glob: module path is not local" end; { eqs with s_gl = Sm.add mp1 eqs.s_gl } @@ -1075,13 +1076,13 @@ and i_eqobs_in_refl env i eqo = | Sraise e -> add_eqs_refl env PV.empty e - | Sabstract _ -> assert false + | Sabstract _ -> invalid_arg "i_eqobs_in_refl: abstract statement" and eqobs_inF_refl env f' eqo = let f = NormMp.norm_xfun env f' in let ffun = Fun.by_xpath f env in match ffun.f_def with - | FBalias _ -> assert false + | FBalias _ -> invalid_arg "eqobs_inF_refl: alias after normalization" | FBdef fdef -> let eqo = match fdef.f_ret with diff --git a/src/ecProofTerm.ml b/src/ecProofTerm.ml index 9055f24629..1a3d1bae7d 100644 --- a/src/ecProofTerm.ml +++ b/src/ecProofTerm.ml @@ -807,7 +807,7 @@ and apply_pterm_to_local ?loc pt id = | LD_mem _ -> apply_pterm_to_arg_r ?loc pt (PVAMemory id) - | LD_abs_st _ -> assert false + | LD_abs_st _ -> invalid_arg "apply_pterm_to_local: abstract statement" (* -------------------------------------------------------------------- *) and process_implicits ip ({ ptev_pt = pt; ptev_env = env; } as pe) = diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 266b86dc87..857667761f 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -297,7 +297,7 @@ let (_i_inuse, s_inuse, se_inuse) = se_inuse map e | Sabstract _ -> - assert false (* FIXME *) + invalid_arg "i_inuse: unexpected abstract statement" and s_inuse (map : uses) (s : stmt) = List.fold_left i_inuse map s.s_node diff --git a/src/phl/ecPhlFel.ml b/src/phl/ecPhlFel.ml index b3cbef12c7..4d2bed4896 100644 --- a/src/phl/ecPhlFel.ml +++ b/src/phl/ecPhlFel.ml @@ -105,7 +105,9 @@ and callable_oracles_i env modv os i = | Sasgn _ | Srnd _ | Sraise _ -> os - | Sabstract _ -> assert false (* FIXME *) + | Sabstract id -> + let us = AbsStmt.byid id env in + List.fold_left (callable_oracles_f env modv) os us.aus_calls let callable_oracles_stmt env modv = callable_oracles_s env modv EcPath.Sx.empty diff --git a/src/phl/ecPhlSkip.ml b/src/phl/ecPhlSkip.ml index 102ca1d1e9..e3a63d13de 100644 --- a/src/phl/ecPhlSkip.ml +++ b/src/phl/ecPhlSkip.ml @@ -45,7 +45,7 @@ module LowInternal = struct if not (List.is_empty bhs.bhs_s.s_node) then tc_error !!tc "instruction list is not empty"; if bhs.bhs_cmp <> FHeq && bhs.bhs_cmp <> FHge then - tc_error !!tc ""; + tc_error !!tc "skip requires comparison to be = or >=, got <="; let concl = map_ss_inv2 f_imp (bhs_pr bhs) (bhs_po bhs) in let concl = EcSubst.f_forall_mems_ss_inv bhs.bhs_m concl in