From 39ddf2a81faa24503956f3cb8c990bb80853cfc2 Mon Sep 17 00:00:00 2001 From: John Harrison Date: Wed, 25 Feb 2026 00:11:03 +0000 Subject: [PATCH] Improve OCaml version robustness and exception safety in proof code Replace newer OCaml library functions (Option.*, List.filter_map, List.concat_map, List.is_empty, String.starts_with/ends_with, Int.logand/shift_right/shift_left) with equivalents available in OCaml 4.05. Add compatibility shims in common/for_hollight.ml. Fix camlp5 parse errors: remove return type annotations on fun expressions in elf.ml and safety.ml, replace `let open Compute in` with top-level `open Compute` in arm/proofs/decode.ml. Fix non-exhaustive pattern match in misc.ml CONS_TO_APPEND_CONV that raised Match_failure uncaught by `with Failure _`. Replace `with _ ->` exception handlers with `with Failure _ ->` throughout to avoid inadvertently catching Sys.Break and other non-Failure exceptions. Co-Authored-By: Claude Opus 4.6 --- arm/proofs/arm.ml | 16 +++---- arm/proofs/bignum_emontredc_8n_cdiff.ml | 50 ++++++++++---------- arm/proofs/decode.ml | 11 +++-- arm/proofs/edwards25519_epadd.ml | 2 +- arm/proofs/edwards25519_epadd_alt.ml | 2 +- arm/proofs/equiv.ml | 52 ++++++++++----------- arm/proofs/p256_montjadd.ml | 4 +- arm/proofs/p256_montjdouble.ml | 4 +- arm/proofs/p384_montjadd.ml | 4 +- arm/proofs/p384_montjdouble.ml | 4 +- arm/proofs/simulator.ml | 6 +-- arm/proofs/simulator_iclasses.ml | 4 +- common/components.ml | 14 +++--- common/consttime.ml | 34 +++++++------- common/elf.ml | 18 +++---- common/equiv.ml | 62 ++++++++++++------------- common/for_hollight.ml | 40 +++++++++++++++- common/misc.ml | 17 ++++--- common/relational.ml | 4 +- common/safety.ml | 2 +- tools/x86_safety_spec_generator.ml | 4 +- x86/proofs/consttime.ml | 8 ++-- x86/proofs/decode.ml | 8 ++-- x86/proofs/edwards25519_epadd.ml | 2 +- x86/proofs/edwards25519_epadd_alt.ml | 2 +- x86/proofs/equiv.ml | 4 +- x86/proofs/mlkem_reduce.ml | 2 +- x86/proofs/mlkem_tobytes.ml | 2 +- x86/proofs/simulator.ml | 10 ++-- x86/proofs/x86.ml | 22 ++++----- x86/tutorial/rel_equivtac.ml | 2 +- 31 files changed, 228 insertions(+), 188 deletions(-) diff --git a/arm/proofs/arm.ml b/arm/proofs/arm.ml index e770a7e56..592427b54 100644 --- a/arm/proofs/arm.ml +++ b/arm/proofs/arm.ml @@ -355,7 +355,7 @@ let ARM_THM = with Failure _ -> failwith ("ARM_THM: Cannot decompose PC expression: " ^ (string_of_term (concl pc_th))) in let _ = if !arm_print_log then - let opt = Option.get execth2.(pc_ofs) in + let opt = option_get execth2.(pc_ofs) in (* opt: |- forall ... aligned_bytes_loaded .. ==> arm_decode .. (arm_INST ..) *) let t = snd (strip_forall (concl (opt))) in @@ -364,7 +364,7 @@ let ARM_THM = Printf.printf "Instruction at `pc + %d (%#x)`: `%s`\n" pc_ofs pc_ofs (string_of_term term) in - MATCH_MP th (MATCH_MP (Option.get execth2.(pc_ofs)) loaded_mc_th);; + MATCH_MP th (MATCH_MP (option_get execth2.(pc_ofs)) loaded_mc_th);; let ARM_ENSURES_SUBLEMMA_TAC = ENSURES_SUBLEMMA_TAC o MATCH_MP aligned_bytes_loaded_update o CONJUNCT1;; @@ -397,13 +397,13 @@ let ARM_CONV (decode_ths:thm option array) (ths:thm list) tm = (fun th -> (* do not use term_match because it is slow. *) let c = concl th in is_eq c && is_read_pc (fst (dest_eq c))) - ths with _ -> failwith "ARM_CONV: can't find `read PC .. = ..` from ths" in + ths with Failure _ -> failwith "ARM_CONV: can't find `read PC .. = ..` from ths" in (* Find `aligned_bytes_loaded ..`. *) let aligned_bytes_loaded_mc_ths:thm list = (* Pick the _mc const from decode_ths, if decode_ths[0] != None, which is likely to be true. *) - let the_mc:term option = Option.bind decode_ths.(0) + let the_mc:term option = option_bind decode_ths.(0) (fun th -> (* th is `forall .., bytes_loaded ... _mc ==> arm_decode ..`. *) let t = concl th in @@ -417,11 +417,11 @@ let ARM_CONV (decode_ths:thm option array) (ths:thm list) tm = let cc = concl th in is_comb cc && ( let c,args = strip_comb (concl th) in c = aligned_bytes_loaded_tm && - (the_mc = None || last args = Option.get the_mc))) + (the_mc = None || last args = option_get the_mc))) ths in if res = [] then failwith ("ARM_CONV: can't find `aligned_bytes_loaded .. .. " ^ - (if the_mc <> None then string_of_term (Option.get the_mc) else "..") + (if the_mc <> None then string_of_term (option_get the_mc) else "..") ^ "` from ths") else res in @@ -821,7 +821,7 @@ let ARM_SUBROUTINE_SIM_TAC ?(is_safety_thm=false) = and svar0 = mk_var("s",`:armstate`) in let ilist = map (vsubst[svar,svar0]) ilist0 in let subth_specl = - try SPECL ilist subth with _ -> begin + try SPECL ilist subth with Failure _ -> begin (if (!arm_print_log) then (Printf.printf "ilist and subth's forall vars do not match\n"; Printf.printf "ilist: [%s]\n" (end_itlist @@ -1019,7 +1019,7 @@ let check_forallvars_tac:tactic = let find_and_check (lhs_pat:term) (t:term) (quants:term list) = let read_eq = try Some (find_term (fun t -> is_eq t && can (term_match [] lhs_pat) (lhs t)) t) - with _ -> None in + with Failure _ -> None in match read_eq with | Some read_eq -> let the_var = rhs read_eq in diff --git a/arm/proofs/bignum_emontredc_8n_cdiff.ml b/arm/proofs/bignum_emontredc_8n_cdiff.ml index 21f1b0a92..450b1ad84 100644 --- a/arm/proofs/bignum_emontredc_8n_cdiff.ml +++ b/arm/proofs/bignum_emontredc_8n_cdiff.ml @@ -1332,20 +1332,20 @@ let precalc_sign_template = let precalc_diffs = let full_expr = mk_list - (List.concat_map (fun (i0, i1) -> + (flat (map (fun (i0, i1) -> let absdiff, isneg = cdiff_from_bignum `n:num` `i_div_4:num` i0 i1 in [absdiff; subst [isneg, mk_var("__isnonneg__",`:bool`)] precalc_sign_template]) - [(1,0);(2,0);(3,0);(2,1);(3,1);(3,2)], + [(1,0);(2,0);(3,0);(2,1);(3,1);(3,2)]), `:(64)word`) in new_definition (subst [full_expr,`__full_expr__:((64)word)list`] `precalc_diffs (n:num) (i_div_4:num) = (__full_expr__:((64)word)list)`);; let precalc_diffs_rev = let full_expr = mk_list - (List.concat_map (fun (i0, i1) -> + (flat (map (fun (i0, i1) -> let absdiff, isneg = cdiff_from_bignum `n:num` `i_div_4:num` i0 i1 in [absdiff; subst [isneg, mk_var("__isnonneg__",`:bool`)] precalc_sign_template]) - [(0,1);(0,2);(0,3);(1,2);(1,3);(2,3)], + [(0,1);(0,2);(0,3);(1,2);(1,3);(2,3)]), `:(64)word`) in new_definition (subst [full_expr,`__full_expr__:((64)word)list`] `precalc_diffs_rev (n:num) (i_div_4:num) = (__full_expr__:((64)word)list)`);; @@ -3119,24 +3119,24 @@ let extend_first_equiv_for_seq_composition equiv_th1 equiv_th2 let ts = find_terms (fun t -> is_comb t && name_of (fst (dest_comb t)) = "mk_equiv_regs") body in - let equiv_regs = List.concat_map (fun t -> let regs = snd (dest_comb t) in - dest_list regs) ts in + let equiv_regs = flat (map (fun t -> let regs = snd (dest_comb t) in + dest_list regs) ts) in (* mk_equiv_regs2 can specify equivalent regs too. *) let ts' = find_terms (fun t -> is_comb t && let t = fst (dest_comb t) in is_comb t && name_of (fst (dest_comb t)) = "mk_equiv_regs2") body in - let equiv_regs2 = List.concat_map (fun t -> + let equiv_regs2 = flat (map (fun t -> let _,(ls1::ls2::[]) = strip_comb t in let regs1,regs2 = dest_list ls1,dest_list ls2 in let pairs = zip regs1 regs2 in - map fst (filter (fun (t1,t2) -> t1 = t2) pairs)) ts' in + map fst (filter (fun (t1,t2) -> t1 = t2) pairs)) ts') in (* some registers that are read. *) let ts2 = find_terms (fun t -> is_comb t && name_of (fst (dest_comb t)) = "read") body in - let specified_regs = List.filter_map (fun t -> + let specified_regs = filter_map (fun t -> let r = snd (dest_comb t) in if is_const r then Some r else None) ts2 in (equiv_regs @ equiv_regs2,specified_regs) in @@ -4370,8 +4370,8 @@ let regs_no_abbrev_left = let addr_regs = (pcend,`X27`)::addr_regs in (* loop counter *) let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP3_EXEC) [pcbeg,pcend] (map (fun (x,y) -> x,[y]) addr_regs)) in - List.map (fun pcdiv4 -> - try assoc (pcdiv4 * 4) res with _ -> []) + map (fun pcdiv4 -> + try assoc (pcdiv4 * 4) res with Failure _ -> []) ((pcbeg / 4) -- (pcend / 4));; let regs_no_abbrev_right = @@ -4383,8 +4383,8 @@ let regs_no_abbrev_right = let addr_regs = (pcend,`X27`)::addr_regs in (* loop counter *) let res = tl (backward_taint_analysis (snd BIGNUM_EMONTREDC_8N_CDIFF_EXEC) [pcbeg,pcend] (map (fun (x,y) -> x,[y]) addr_regs)) in - List.map (fun pcdiv4 -> - try assoc (pcdiv4 * 4) res with _ -> []) + map (fun pcdiv4 -> + try assoc (pcdiv4 * 4) res with Failure _ -> []) ((pcbeg / 4) -- (pcend / 4));; @@ -4668,8 +4668,8 @@ let step3_outerloop_out_regs_left,step3_outerloop_out_regs_right = (Array.of_list inst_map) step3_outerloop_out_regs_right in let lr = zip m step3_outerloop_out_regs_right in - let lr = List.filter_map (fun x,y -> - if x = None then None else Some (snd (Option.get x),y)) lr in + let lr = filter_map (fun x,y -> + if x = None then None else Some (snd (option_get x),y)) lr in unzip lr;; let step3_outerloop_eqout_regs = build_equiv_regs2 @@ -4729,7 +4729,7 @@ let regs_no_abbrev_left = let addr_regs = (pcend,[`X27`;`X0`;`X1`;`X2`;`SP`;`X30`])::addr_regs in let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP3_EXEC) [pcbeg,pcend] addr_regs) in - List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> []) + map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> []) ((pcbeg / 4) -- (pcend / 4));; let regs_no_abbrev_right = @@ -4745,7 +4745,7 @@ let regs_no_abbrev_right = addr_regs in let res = tl (backward_taint_analysis (snd BIGNUM_EMONTREDC_8N_CDIFF_EXEC) [pcbeg,pcend] addr_regs) in - List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> []) + map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> []) ((pcbeg / 4) -- (pcend / 4));; @@ -4935,8 +4935,8 @@ let step3_inner_loop_postamble_out_regs_left, (Array.of_list inst_map) step3_inner_loop_postamble_out_regs_right in let lr = zip m step3_inner_loop_postamble_out_regs_right in - let lr = List.filter_map (fun x,y -> - if x = None then None else Some (snd (Option.get x),y)) lr in + let lr = filter_map (fun x,y -> + if x = None then None else Some (snd (option_get x),y)) lr in unzip lr;; let step3_inner_loop_postamble_eqout_regs = build_equiv_regs2 @@ -5001,7 +5001,7 @@ let regs_no_abbrev_left = let addr_regs = update_key_list pcend [`X0`;`X1`;`X2`;`SP`;`X30`;`X26`] addr_regs in let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP3_EXEC) [pcbeg,pcend] addr_regs) in - List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> []) + map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> []) ((pcbeg / 4) -- (pcend / 4));; let regs_no_abbrev_right = @@ -5015,7 +5015,7 @@ let regs_no_abbrev_right = let addr_regs = update_key_list pcend [`X0`;`X1`;`X2`;`SP`;`X30`;`X26`] addr_regs in let res = tl (backward_taint_analysis (snd BIGNUM_EMONTREDC_8N_CDIFF_EXEC) [pcbeg,pcend] addr_regs) in - List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> []) + map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> []) ((pcbeg / 4) -- (pcend / 4));; @@ -5567,7 +5567,7 @@ let regs_no_abbrev_left = [`X27`;`X0`;`X1`;`X2`;`SP`;`X30`] addr_regs in let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP1_EXEC) [pcbeg,pcend] addr_regs) in - List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> []) + map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> []) ((pcbeg / 4) -- (pcend / 4));; let regs_no_abbrev_right = @@ -5582,7 +5582,7 @@ let regs_no_abbrev_right = [`X27`;`X0`;`X1`;`X2`;`SP`;`X30`] addr_regs in let res = tl (backward_taint_analysis (snd MADDLOOP_STEP2_X30_EXEC) [pcbeg,pcend] addr_regs) in - List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> []) + map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> []) ((pcbeg / 4) -- (pcend / 4));; @@ -5994,7 +5994,7 @@ let regs_no_abbrev = let addr_regs = (pcend,[`X27`;`X0`;`X1`;`X2`;`SP`;`X30`])::addr_regs in let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP1_EXEC) [pcbeg,pcend] addr_regs) in - List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> []) + map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> []) ((pcbeg / 4) -- (pcend / 4));; @@ -6215,7 +6215,7 @@ let regs_no_abbrev = let addr_regs = update_key_list pcend [`X0`;`X1`;`X2`;`SP`;`X30`;`X26`] addr_regs in let res = tl (backward_taint_analysis (snd OUTERLOOP_STEP1_EXEC) [pcbeg,pcend] addr_regs) in - List.map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with _ -> []) + map (fun pcdiv4 -> try assoc (pcdiv4 * 4) res with Failure _ -> []) ((pcbeg / 4) -- (pcend / 4));; (* (state number, (equation, fresh var)) *) diff --git a/arm/proofs/decode.ml b/arm/proofs/decode.ml index f8f201940..14a415d56 100644 --- a/arm/proofs/decode.ml +++ b/arm/proofs/decode.ml @@ -1208,7 +1208,7 @@ let ALIAS_CONV = let th' = INST_TYPE (map (fun ty' -> ty,ty') (type_vars_in_term (concl th))) th in try f (CONV_RULE (CHANGED_CONV (REWRITE_CONV [SYM xth])) th') - with _ -> I in + with Failure _ -> I in g `:64` XZR_ZR o g `:32` WZR_ZR o f th in let f th = if can (find_term @@ -1244,8 +1244,9 @@ let ALIAS_CONV = self := ONCE_DEPTH_CONV (REWRITES_CONV net); OPERAND_ALIAS_CONV THENC ALIAS_CONV;; +open Compute;; + let PURE_DECODE_CONV = - let open Compute in let custom_word_red_conv_list = (* No WORD_IWORD_CONV *) @@ -1320,12 +1321,12 @@ let PURE_DECODE_CONV = let c = concl th in (* c should be: `decode .. = SOME ...` *) let r,_ = dest_comb (rhs c) in if is_const r && name_of r = "SOME" then th else failwith "" - with _ -> failwith ("PURE_DECODE_CONV: " ^ (string_of_term t));; + with Failure _ -> failwith ("PURE_DECODE_CONV: " ^ (string_of_term t));; let DECODE_CONV tm = let th = PURE_DECODE_CONV tm in try CONV_RULE (RAND_CONV (RAND_CONV ALIAS_CONV)) th - with _ -> th;; + with Failure _ -> th;; (* ------------------------------------------------------------------------- *) (* Testing and preparation. *) @@ -1733,7 +1734,7 @@ let term_of_relocs_arm, assert_relocs = assert false) in pc+4, next_insns - with _ -> failwith ("could not check opcode " ^ (string_of_term reloc_opcode)) in + with Failure _ -> failwith ("could not check opcode " ^ (string_of_term reloc_opcode)) in (* opcode_fn is the large OCaml function printed by print_literal_relocs_from_elf *) fun (args,tm) opcode_fn -> diff --git a/arm/proofs/edwards25519_epadd.ml b/arm/proofs/edwards25519_epadd.ml index 0df1f08bd..d838ed8da 100644 --- a/arm/proofs/edwards25519_epadd.ml +++ b/arm/proofs/edwards25519_epadd.ml @@ -3151,7 +3151,7 @@ let EDWARDS25519_EPADD_CORRECT = time prove MAP_EVERY X_GEN_TAC [`x1:int`; `y1:int`; `x2:int`; `y2:int`] THEN STRIP_TAC THEN EVERY_ASSUM(fun th -> try STRIP_ASSUME_TAC(MATCH_MP EDWARDS25519_EXPROJECTIVE_BOUND th) - with _ -> ALL_TAC) THEN + with Failure _ -> ALL_TAC) THEN DISCARD_STATE_TAC "s39" THEN DISCARD_MATCHING_ASSUMPTIONS [`aligned a b`; `nonoverlapping_modulo a b c`] THEN diff --git a/arm/proofs/edwards25519_epadd_alt.ml b/arm/proofs/edwards25519_epadd_alt.ml index a1889362b..8287edfe3 100644 --- a/arm/proofs/edwards25519_epadd_alt.ml +++ b/arm/proofs/edwards25519_epadd_alt.ml @@ -1790,7 +1790,7 @@ let EDWARDS25519_EPADD_ALT_CORRECT = time prove MAP_EVERY X_GEN_TAC [`x1:int`; `y1:int`; `x2:int`; `y2:int`] THEN STRIP_TAC THEN EVERY_ASSUM(fun th -> try STRIP_ASSUME_TAC(MATCH_MP EDWARDS25519_EXPROJECTIVE_BOUND th) - with _ -> ALL_TAC) THEN + with Failure _ -> ALL_TAC) THEN DISCARD_STATE_TAC "s39" THEN DISCARD_MATCHING_ASSUMPTIONS [`aligned a b`; `nonoverlapping_modulo a b c`] THEN diff --git a/arm/proofs/equiv.ml b/arm/proofs/equiv.ml index 35e1797e9..03ef4d93b 100644 --- a/arm/proofs/equiv.ml +++ b/arm/proofs/equiv.ml @@ -27,12 +27,12 @@ let get_bytelist_length (ls:term): int = "get_bytelist_length: cannot get the length of `%s`" (string_of_term ls));; let define_mc_from_intlist (newname:string) (ops:int list) = - let charlist = List.concat_map + let charlist = flat (map (fun op32 -> - [Char.chr (Int.logand op32 255); - Char.chr (Int.logand (Int.shift_right op32 8) 255); - Char.chr (Int.logand (Int.shift_right op32 16) 255); - Char.chr (Int.logand (Int.shift_right op32 24) 255)]) ops in + [Char.chr (op32 land 255); + Char.chr ((op32 lsr 8) land 255); + Char.chr ((op32 lsr 16) land 255); + Char.chr ((op32 lsr 24) land 255)]) ops) in let byte_list = Bytes.init (List.length charlist) (fun i -> List.nth charlist i) in define_word_list newname (term_of_bytes byte_list);; @@ -106,7 +106,7 @@ let DIVIDES_EXP_CONV (divisor:term) (dividend:term): thm = try let lth = fn divisor lhs in ISPEC rhs (MATCH_MP DIVIDES_RMUL lth) - with _ -> + with Failure _ -> let lhs,rhs = dest_binary "*" dividend in let rth = fn divisor rhs in ISPEC lhs (MATCH_MP DIVIDES_LMUL rth) @@ -166,8 +166,8 @@ let DIV_EXP_REDUCE_CONV (dividend:term) (divisor:term):thm = (* `(lhs + rhs) DIV divisor = (lhs DIV divisor) + (rhs DIV divisor)` *) let precond = try DISJ1 (DIVIDES_EXP_CONV divisor lhs) (mk_binary "num_divides" (divisor,rhs)) - with _ -> try DISJ2 (mk_binary "num_divides" (divisor,lhs)) (DIVIDES_EXP_CONV divisor rhs) - with _ -> failwith "Could not derive DIV_ADD's precond" in + with Failure _ -> try DISJ2 (mk_binary "num_divides" (divisor,lhs)) (DIVIDES_EXP_CONV divisor rhs) + with Failure _ -> failwith "Could not derive DIV_ADD's precond" in let expr = REWRITE_CONV[MATCH_MP DIV_ADD precond] expr in (* (lhs DIV divisor) + (rhs DIV divisor) = lhs' + rhs' *) REWRITE_RULE [lhs_eq;rhs_eq;simp_one] expr @@ -576,13 +576,13 @@ let equiv_test_ops: int list = [ ];; let equiv_test_mc = - let charlist = List.concat_map + let charlist = flat (map (fun op32 -> - [Char.chr (Int.logand op32 255); - Char.chr (Int.logand (Int.shift_right op32 8) 255); - Char.chr (Int.logand (Int.shift_right op32 16) 255); - Char.chr (Int.logand (Int.shift_right op32 24) 255)]) - equiv_test_ops in + [Char.chr (op32 land 255); + Char.chr ((op32 lsr 8) land 255); + Char.chr ((op32 lsr 16) land 255); + Char.chr ((op32 lsr 24) land 255)]) + equiv_test_ops) in let byte_list = Bytes.init (List.length charlist) (fun i -> List.nth charlist i) in define_word_list "__equiv_test_mc" (term_of_bytes byte_list);; @@ -620,7 +620,7 @@ let backward_taint_analysis (* Input and output components *) for i = pc_end downto pc_begin do (* mark tainted_regs[i] as tainted *) - let ts = try assoc i tainted_regs with _ -> [] in + let ts = try assoc i tainted_regs with Failure _ -> [] in tainted := union !tainted ts; match decode_ths.(i) with | None -> () @@ -752,7 +752,7 @@ let map_output_regs match update_idx with | Some update_idx -> begin (* found! *) - let the_th_left = Option.get (decode_ths_left.(pc_begin_left + (idx_left-1)*4)) in + let the_th_left = option_get (decode_ths_left.(pc_begin_left + (idx_left-1)*4)) in let r_left = snd (dest_imp (snd (strip_forall (concl the_th_left)))) in let f,args_left = strip_comb r_left in if name_of f <> "arm_decode" then failwith "Unknown inst" else @@ -1215,7 +1215,7 @@ let ARM_N_STEPS_AND_REWRITE_TAC execth (snums:int list) (inst_map: int list) if List.length abbrevs_for_st_n = List.length new_state_eqs then (* For each `read c sn = rhs`, replace rhs with abbrev *) - let new_state_eqs = List.filter_map + let new_state_eqs = filter_map (fun new_state_eq -> let rhs = rhs (concl new_state_eq) in (* Find 'rhs = abbrev' from the left program's updates. *) @@ -1225,7 +1225,7 @@ let ARM_N_STEPS_AND_REWRITE_TAC execth (snums:int list) (inst_map: int list) | Some (_,rhs_to_abbrev) -> (try Some (GEN_REWRITE_RULE RAND_CONV [rhs_to_abbrev] new_state_eq) - with _ -> + with Failure _ -> (Printf.printf "Failed to proceed.\n"; Printf.printf "- rhs: `%s`\n" (string_of_term rhs); Printf.printf "- rhs_to_abbrev: `%s`\n" (string_of_thm rhs_to_abbrev); @@ -1298,7 +1298,7 @@ let TRY_CONST_PCS_TAC (pcs:int list) (val_word_ptrs:term list):tactic = else if is_binary "<=" t then Some ("<=",dest_binary "<=" t) else None in fun (asl,w) -> - let upper_lower_bounds = List.filter_map + let upper_lower_bounds = filter_map (fun _,th -> let c = concl th in match decomp_relop c with @@ -1309,11 +1309,11 @@ let TRY_CONST_PCS_TAC (pcs:int list) (val_word_ptrs:term list):tactic = | _ -> None) asl in let ranges = List.map (fun val_word_ptr -> - let lb = List.filter_map (fun t,comp,i -> + let lb = filter_map (fun t,comp,i -> if comp = ">=" && t = val_word_ptr then Some i else None) upper_lower_bounds in let lb = List.fold_left max 0 lb in - let ub = List.filter_map (fun t,comp,i -> + let ub = filter_map (fun t,comp,i -> if comp = "<" && t = val_word_ptr then Some i else None) upper_lower_bounds in let ub = List.fold_left min max_int ub in @@ -1370,7 +1370,7 @@ let FIND_HOLE_TAC: tactic = let terms_nonoverlap, term_divides = (butlast goal_conjs, last goal_conjs) in if fst (strip_comb term_divides) <> `divides` then failwith ("Not 'divides' predicate: " ^ (string_of_term term_divides)) else - let ranges:(term*int) list = List.concat_map + let ranges:(term*int) list = flat (map (fun t -> let tt,ranges = strip_comb t in if tt <> `nonoverlapping_modulo` then @@ -1384,7 +1384,7 @@ let FIND_HOLE_TAC: tactic = then failwith ("Has non-constant size: " ^ (string_of_term t)) else (ptr, dest_small_numeral size) in List.map dest_range (List.tl ranges)) - terms_nonoverlap in + terms_nonoverlap) in let ranges = uniq (sort (<) ranges) in Printf.printf "Aggregated ranges: %s\n" (String.concat ", " (List.map @@ -1698,7 +1698,7 @@ let EVENTUALLY_TAKE_STEP_RIGHT_FORALL_TAC exec_decode (k:int):tactic = DISCH_THEN (fun th -> try let _,th2 = CONJ_PAIR th in LABEL_TAC "HEVENTUALLY" th2 - with _ -> + with Failure _ -> (Printf.printf "Not a conjunction: %s\n" (string_of_thm th); failwith "EVENTUALLY_TAKE_STEP_RIGHT_FORALL_TAC")) THEN DISCH_THEN (LABEL_TAC "HSTEPS") THEN @@ -2332,7 +2332,7 @@ needs "common/actions_merger.ml";; let rec break_equal_loads actions (decodeth1:thm option array) pcbegin1 (decodeth2:thm option array) pcbegin2 = let get_opname_from_decode (th:thm option):string = - let th = Option.get th in + let th = option_get th in (* th is: `|- forall s pc. aligned_bytes_loaded s (word pc) bignum_montsqr_p256_mc ==> arm_decode s (word (pc + 216)) (arm_ADC X8 X8 XZR)` *) @@ -2368,7 +2368,7 @@ let rec break_equal_loads actions (decodeth1:thm option array) pcbegin1 let opname2 = get_opname_from_decode decodeth2.(pcbegin2 + 4 * (beg2 + i)) in if opname1 <> opname2 then failwith (Printf.sprintf "Op not equal: %s vs. %s" opname1 opname2) else - if String.starts_with ~prefix:"arm_LD" opname1 then + if starts_with "arm_LD" opname1 then if !ld_start_i = -1 then begin (* first load *) (* flush ("equal", eq_start_i ~ i-1) *) diff --git a/arm/proofs/p256_montjadd.ml b/arm/proofs/p256_montjadd.ml index 7d1fa504d..6f72e719a 100644 --- a/arm/proofs/p256_montjadd.ml +++ b/arm/proofs/p256_montjadd.ml @@ -1179,9 +1179,9 @@ orthogonal_components_conv_custom_cache := try let lref = assoc l !cache in try Some (assoc r !lref) - with _ -> let newth = eval () in + with Failure _ -> let newth = eval () in lref := (r,newth)::!lref; Some newth - with _ -> let newth = eval () in + with Failure _ -> let newth = eval () in cache := (l, ref [(r,newth)])::!cache; Some newth;; diff --git a/arm/proofs/p256_montjdouble.ml b/arm/proofs/p256_montjdouble.ml index 3faf9bfab..86464d2cf 100644 --- a/arm/proofs/p256_montjdouble.ml +++ b/arm/proofs/p256_montjdouble.ml @@ -1910,9 +1910,9 @@ orthogonal_components_conv_custom_cache := try let lref = assoc l !cache in try Some (assoc r !lref) - with _ -> let newth = eval () in + with Failure _ -> let newth = eval () in lref := (r,newth)::!lref; Some newth - with _ -> let newth = eval () in + with Failure _ -> let newth = eval () in cache := (l, ref [(r,newth)])::!cache; Some newth;; diff --git a/arm/proofs/p384_montjadd.ml b/arm/proofs/p384_montjadd.ml index 7b74dc450..8e256d9b8 100644 --- a/arm/proofs/p384_montjadd.ml +++ b/arm/proofs/p384_montjadd.ml @@ -1578,9 +1578,9 @@ orthogonal_components_conv_custom_cache := try let lref = assoc l !cache in try Some (assoc r !lref) - with _ -> let newth = eval () in + with Failure _ -> let newth = eval () in lref := (r,newth)::!lref; Some newth - with _ -> let newth = eval () in + with Failure _ -> let newth = eval () in cache := (l, ref [(r,newth)])::!cache; Some newth;; diff --git a/arm/proofs/p384_montjdouble.ml b/arm/proofs/p384_montjdouble.ml index 01e4a3749..e109951e9 100644 --- a/arm/proofs/p384_montjdouble.ml +++ b/arm/proofs/p384_montjdouble.ml @@ -2603,9 +2603,9 @@ orthogonal_components_conv_custom_cache := try let lref = assoc l !cache in try Some (assoc r !lref) - with _ -> let newth = eval () in + with Failure _ -> let newth = eval () in lref := (r,newth)::!lref; Some newth - with _ -> let newth = eval () in + with Failure _ -> let newth = eval () in cache := (l, ref [(r,newth)])::!cache; Some newth;; diff --git a/arm/proofs/simulator.ml b/arm/proofs/simulator.ml index e69bebcc2..b8fb1ced3 100755 --- a/arm/proofs/simulator.ml +++ b/arm/proofs/simulator.ml @@ -257,8 +257,8 @@ let cosimulate_instructions (memopidx: int option) icodes = let execth = ARM_MK_EXEC_RULE(REFL ibyteterm) in let decoded = mk_flist - (map (rand o rand o snd o strip_forall o concl o Option.get) - (filter Option.is_some (Array.to_list (snd execth)))) + (map (rand o rand o snd o strip_forall o concl o option_get) + (filter option_is_some (Array.to_list (snd execth)))) and result = can prove (goal, @@ -529,7 +529,7 @@ let cosimulate_ld1r() = let stackoff = if rn = 31 then Random.int 14 * 16 else Random.int 224 in - let stackoff' = (Int.shift_left 8 size)/8 + stackoff in + let stackoff' = (8 lsl size)/8 + stackoff in let code = pow2 30 */ num q +/ pow2 12 */ num 0b001101110111111100 +/ diff --git a/arm/proofs/simulator_iclasses.ml b/arm/proofs/simulator_iclasses.ml index 11221bef6..f099b0ea2 100644 --- a/arm/proofs/simulator_iclasses.ml +++ b/arm/proofs/simulator_iclasses.ml @@ -574,7 +574,7 @@ let check_insns () = | Some idx -> let hexcode = "0x" ^ (String.sub l 0 idx) in let desc = String.trim (String.sub l (idx+1) (String.length l - idx - 1)) in - if String.starts_with ~prefix:".word" desc then true (* defines a constant *) + if starts_with ".word" desc then true (* defines a constant *) else try let opcode = int_of_string hexcode in @@ -582,7 +582,7 @@ let check_insns () = true (* Check passes *) else List.exists (match_bitpattern opcode) iclasses - with _ -> false + with Failure _ -> false in let tmppath = Filename.temp_file "objdump" ".txt" in diff --git a/common/components.ml b/common/components.ml index c6338132a..430a610a2 100644 --- a/common/components.ml +++ b/common/components.ml @@ -2656,7 +2656,7 @@ let (COMPONENT_CANON_CONV:conv),add_component_alias_thms = (fun tm -> if is_const tm then try assoc tm !component_canon_conv_cache - with _ -> + with Failure _ -> let thnew = !conv tm in component_canon_conv_cache := (tm,thnew)::!component_canon_conv_cache; thnew @@ -2953,9 +2953,9 @@ let ORTHOGONAL_COMPONENTS_CONV tm = try let lref = assoc lhs !orthogonal_components_conv_cache in try assoc rhs !lref - with _ -> let newth = eval() in lref := (rhs, newth)::!lref; + with Failure _ -> let newth = eval() in lref := (rhs, newth)::!lref; newth - with _ -> let newth = eval() in + with Failure _ -> let newth = eval() in orthogonal_components_conv_cache := (lhs, ref [(rhs,newth)])::!orthogonal_components_conv_cache; newth else begin @@ -2963,7 +2963,7 @@ let ORTHOGONAL_COMPONENTS_CONV tm = | Some th -> th | None -> eval() end - with _ -> failwith "ORTHOGONAL_COMPONENTS_CONV: unknown term";; + with Failure _ -> failwith "ORTHOGONAL_COMPONENTS_CONV: unknown term";; let ORTHOGONAL_COMPONENTS_RULE2 tm1 tm2 = ORTHOGONAL_COMPONENTS_CONV(list_mk_icomb "orthogonal_components" [tm1;tm2]);; @@ -3488,11 +3488,11 @@ let COMPONENT_READ_OVER_WRITE_CONV = (try let th = rule_same tm in rule_same_matched := true; MP th (VALID_COMPONENT_CONV(lhand(concl th))) - with _ -> + with Failure _ -> try let th = rule_orth tm in rule_orth_matched := true; MP th (orth_rule(lhand(concl th))) - with _ -> + with Failure _ -> (* If tm was of the form `read _ (write _ _ _)`, this failure is from *_COMPONENT{S}_CONV which were supposed to prove either fully overlapping or orthogonal aliasing relation between the reads and @@ -3607,7 +3607,7 @@ let ASSUMPTION_STATE_UPDATE_TAC = STATE_UPDATE_RULE cxt uth thi with Failure failmsg -> (if !components_print_log && - String.starts_with ~prefix:"NONOVERLAPPING_RULE" failmsg then + starts_with "NONOVERLAPPING_RULE" failmsg then (Printf.printf "Info: assumption `%s` is erased.\n" (string_of_term (concl thi)); Printf.printf "- Reason: %s\n" failmsg)); failwith failmsg) thy diff --git a/common/consttime.ml b/common/consttime.ml index e5a315658..bd8b53086 100644 --- a/common/consttime.ml +++ b/common/consttime.ml @@ -25,7 +25,7 @@ let find_stack_access_size (fnspec_maychange:term): (term * int) option = a = stackptr)) fnspec_maychange in let baseptr,sz = dest_pair t in Some (baseptr, dest_small_numeral sz) - with _ -> None;; + with Failure _ -> None;; find_stack_access_size `MAYCHANGE [memory :> bytes (stackpointer,264)]`;; find_stack_access_size `MAYCHANGE [memory :> bytes(z,8 * 8); @@ -66,7 +66,7 @@ let gen_mk_safety_spec let c_to_hol_vars = map (fun ((x,_,_),yvar) -> x,yvar) c_to_hol_vars in try assoc var_c c_to_hol_vars - with _ -> failwith ("c_var_to_hol: unknown var in C: " ^ var_c) in + with Failure _ -> failwith ("c_var_to_hol: unknown var in C: " ^ var_c) in let bytes_loaded_terms = find_terms (fun t -> is_comb t && @@ -78,11 +78,11 @@ let gen_mk_safety_spec let (bytes_loaded_mc::[]),bytes_loaded_others = List.partition (fun t -> let _::pc::_ = snd (strip_comb t) in let word_const,pc_var = dest_comb pc in - String.starts_with ~prefix:"pc" (name_of pc_var)) + starts_with"pc" (name_of pc_var)) bytes_loaded_terms in let read_sp_eq: term option = try Some (find_term find_eq_stackpointer fnspec_precond) - with _ -> None in + with Failure _ -> None in let stack_access_size: (term*int) option = find_stack_access_size fnspec_maychanges in assert ((read_sp_eq = None) = (stack_access_size = None)); @@ -91,11 +91,11 @@ let gen_mk_safety_spec List.find_opt (fun t -> name_of t = "returnaddress") fnspec_quants in let read_x30_eq: term option = try Some (find_term find_eq_returnaddress fnspec_precond) - with _ -> None in + with Failure _ -> None in (* An expression s to a term of :num type. *) let rec elemsz_to_hol (s:string): term = - let s = if String.starts_with ~prefix:">=" s + let s = if starts_with">=" s then String.sub s 2 (String.length s - 2) else s in match String.index_opt s '*' with @@ -106,7 +106,7 @@ let gen_mk_safety_spec mk_binary "*" (elemsz_to_hol expr_lhs, elemsz_to_hol expr_rhs) | None -> (try mk_small_numeral (int_of_string s) - with _ -> + with Failure _ -> let v = c_var_to_hol s in match dest_type (type_of v) with | ("num",_) -> v @@ -118,7 +118,7 @@ let gen_mk_safety_spec (fun (c_varname,range,elemty_size) -> c_var_to_hol c_varname, (try mk_small_numeral (elemty_size * int_of_string range) - with _ -> + with Failure _ -> mk_binary "*" (elemsz_to_hol range, mk_small_numeral elemty_size))) in map fn (meminputs @ memoutputs @ memtemps), @@ -143,9 +143,9 @@ let gen_mk_safety_spec end ) @ (match stack_access_size with - | None -> [`pc:num`] @ (Option.to_list returnaddress_var) + | None -> [`pc:num`] @ (match returnaddress_var with Some v -> [v] | None -> []) | Some (baseptr,sz) -> - [`pc:num`;baseptr] @ (Option.to_list returnaddress_var)) in + [`pc:num`;baseptr] @ (match returnaddress_var with Some v -> [v] | None -> [])) in let f_events = mk_var("f_events", itlist mk_fun_ty (map type_of f_events_public_args) `:(uarch_event)list`) in @@ -226,7 +226,7 @@ let gen_mk_safety_spec (* Return the spec, as well as the HOL Light variables having public info *) (mk_exists(f_events, list_mk_forall(fnspec_quants_filtered, spec_without_quantifiers)), - the_e_var::`pc:num`::public_vars @ Option.to_list returnaddress_var @ + the_e_var::`pc:num`::public_vars @ (match returnaddress_var with Some v -> [v] | None -> []) @ (if read_sp_eq = None then [] else [`stackpointer:int64`]));; let REPEAT_GEN_AND_OFFSET_STACKPTR_TAC = @@ -284,7 +284,7 @@ let DISCHARGE_MEMACCESS_INBOUNDS_USING_ASM_TAC:tactic = is_comb cth && name_of (fst (strip_comb cth)) = "memaccess_inbounds") asl) in - if List.is_empty meminbounds then + if meminbounds = [] then failwith "No memaccess_inbounds assumption" else end_itlist (fun tac1 tac2 -> tac1 ORELSE tac2) (map try_discharge meminbounds));; @@ -461,7 +461,7 @@ let GEN_PROVE_SAFETY_SPEC_TAC = let quantvars,forall_body = strip_forall(snd(dest_exists w)) in let stored_abbrevs = ref [] in - if List.is_empty quantvars || hd quantvars <> `e:(uarch_event)list` + if quantvars = [] || hd quantvars <> `e:(uarch_event)list` then failwith "The goal must be `exists f_events. forall e ...`" else (* The destination PC *) @@ -607,13 +607,13 @@ let CONCRETIZE_F_EVENTS_TAC (concrete_f_events:term): tactic = let free_f_events = frees concrete_f_events in (* Do sanity check *) let _ = List.iter (fun t -> - if not (String.starts_with ~prefix:"f_ev" (name_of t)) + if not (starts_with"f_ev" (name_of t)) then failwith ("This free variable does not start with 'f_ev'; is it a function " ^ "that returns a list of uarch_events?") else let tty = type_of t in try let _ = dest_fun_ty tty in () - with _ -> failwith "This is not a function type") + with Failure _ -> failwith "This is not a function type") free_f_events in let new_goal = subst [concrete_f_events,old_f_events] body in let new_goal = list_mk_exists (free_f_events, new_goal) in @@ -673,7 +673,7 @@ let ENSURES_EVENTS_SEQUENCE_TAC (pc:term) (inv:term): tactic = let e_back::e_front_tail::[] = snd (strip_comb e2_def_post) in - let e2_def_pre = try Some (find_e2_def precond) with _ -> None in + let e2_def_pre = try Some (find_e2_def precond) with Failure _ -> None in let _ = match e2_def_pre with | Some (_,e2_def_pre,_) -> if not (is_nil e2_def_pre || @@ -761,7 +761,7 @@ let ENSURES_EVENTS_WHILE_UP2_TAC = let the_enumeratel,(counter::e_loop::[]) = strip_comb e_enumeratel in (* discard e_back! *) the_enumeratel,counter,e_loop,e_front,e_prev_trace - with _ -> failmsg() in + with Failure _ -> failmsg() in let _ = match numitr with | None -> () diff --git a/common/elf.ml b/common/elf.ml index 233139ac2..4d245887f 100644 --- a/common/elf.ml +++ b/common/elf.ml @@ -108,11 +108,11 @@ let load_elf (arch:int) (reloc_type:int -> 'a) (file:bytes): https://refspecs.linuxbase.org/elf/gabi4+/ch4.sheader.html has a table for their integer values, and Figure 4-14 has types for special sections such as .text . *) - fun name ty:bytes -> + fun name ty -> let hdr = find (fun header -> section_name header = name) headers in check_section_type hdr ty; hdr in - let find_section_contents (name,ty):bytes = + let find_section_contents (name,ty) = section_contents (find_section_header name ty) in (* From .strtab (string table) extract a string whose byte offset starts from @@ -121,7 +121,7 @@ let load_elf (arch:int) (reloc_type:int -> 'a) (file:bytes): try let the_table = section_contents (find_section_header ".strtab" 3 (* SHT_STRTAB *)) in fun chridx -> get_string the_table chridx - with _ -> fun (chridx:int) -> "" in + with Failure _ -> fun (chridx:int) -> "" in (* The .rodata section (None if nonexistent) *) let rodata_contents:bytes option = catch @@ -133,20 +133,20 @@ let load_elf (arch:int) (reloc_type:int -> 'a) (file:bytes): find_section_contents (".symtab",2 (* SHT_SYMTAB *)) in let symbol_name (symtab_idx:int): string = - let symtab = Option.get symtab_contents in + let symtab = option_get symtab_contents in let sym_entrysize = 24 (* size of Elf64_Sym struct *) in let char_idx = get_int_le symtab (symtab_idx * sym_entrysize) 4 in from_string_table char_idx in (* The "st_shndx" field *) let symbol_sectionidx (symtab_idx:int): int = - let symtab = Option.get symtab_contents in + let symtab = option_get symtab_contents in let sym_entrysize = 24 in get_int_le symtab (symtab_idx * sym_entrysize + 6) 2 in (* Least-significant 4 bits of the "st_info" field *) let symbol_type (symtab_idx:int): int = - let symtab = Option.get symtab_contents in + let symtab = option_get symtab_contents in let sym_entrysize = 24 in let symbol_info = get_int_le symtab (symtab_idx * sym_entrysize + 4) 1 in symbol_info land 0xf @@ -333,7 +333,7 @@ let load_macho (cputype:int) (reloc_type:int -> 'a) (file:bytes): (* Some symbols starting with "ltmp" are auto-generated. They are ignored by tools like: https://github.com/microsoft/llvm-mctoll/blob/master/MachODump.cpp#L228 *) - not (String.starts_with ~prefix:"ltmp" symbol_name) + not (starts_with "ltmp" symbol_name) then begin const_symbols := !const_symbols @ [(symbol_name, n_value(*byte offset *))] end) !raw_symbols; @@ -358,11 +358,11 @@ let load_macho (cputype:int) (reloc_type:int -> 'a) (file:bytes): let symname,secofs,seclen = s in if start_ofs < seclen then let symbol_len = if end_ofs <> None - then (Option.get end_ofs - start_ofs) + then (option_get end_ofs - start_ofs) else seclen - start_ofs in Bytes.sub file (secofs + start_ofs) symbol_len else - let end_ofs = Option.map (fun x -> x - seclen) end_ofs in + let end_ofs = option_map (fun x -> x - seclen) end_ofs in extract_bytes (start_ofs - seclen) end_ofs sections' in (* 1. The __text section data *) diff --git a/common/equiv.ml b/common/equiv.ml index d9387b19d..affa9127a 100644 --- a/common/equiv.ml +++ b/common/equiv.ml @@ -45,7 +45,7 @@ let get_memory_read_info = (* args is just a location *) assert (List.length args = 1); Some (List.hd args, bytewidth, accessor) - with _ -> + with Failure _ -> begin match accessor with | "bytes" -> (* args is (loc, len). *) @@ -62,7 +62,7 @@ let get_base_ptr_and_ofs (t:term): term * term = let wordc, ofs = dest_comb y in if name_of wordc <> "word" then failwith "not word" else (baseptr, ofs) - with _ -> (t, mk_small_numeral 0);; + with Failure _ -> (t, mk_small_numeral 0);; assert (get_base_ptr_and_ofs `x:int64` = (`x:int64`,`0`));; assert (get_base_ptr_and_ofs `word_add x (word 32):int64` = (`x:int64`,`32`));; @@ -79,7 +79,7 @@ let get_base_ptr_and_constofs (t:term): term * int = try let ofs = rhs (concl (NUM_RED_CONV ofs)) in (base,dest_small_numeral ofs) - with _ -> (t,0);; + with Failure _ -> (t,0);; assert (get_base_ptr_and_constofs `word_add x (word (8*4)):int64` = (`x:int64`,32));; @@ -107,24 +107,24 @@ let rec MK_MEMORY_READ_EQ_BIGDIGIT_CONV = let const_num_opt (t:term): int option = try if is_numeral t then Some (dest_small_numeral t) else Some (dest_small_numeral (rhs (concl (NUM_RED_CONV t)))) - with _ -> None in + with Failure _ -> None in let eight = `8` in let rec divide_by_8 t: term option = - try Some (mk_small_numeral ((Option.get (const_num_opt t)) / 8)) - with _ -> try + try Some (mk_small_numeral ((option_get (const_num_opt t)) / 8)) + with Failure _ -> try let l,r = dest_binary "*" t in if l = eight then Some r else if r = eight then Some l else None - with _ -> try + with Failure _ -> try let l,r = dest_binary "+" t in match (divide_by_8 l),(divide_by_8 r) with | Some l', Some r' -> Some (mk_binary "+" (l',r')) | _ -> None - with _ -> try + with Failure _ -> try let l,r = dest_binary "-" t in match (divide_by_8 l),(divide_by_8 r) with | Some l', Some r' -> Some (mk_binary "-" (l',r')) | _ -> None - with _ -> None + with Failure _ -> None in let is_multiple_of_8 t = divide_by_8 t <> None in let subtract_num t1 t2: term option = @@ -133,7 +133,7 @@ let rec MK_MEMORY_READ_EQ_BIGDIGIT_CONV = else (* returns: ((sym expr, coeff) list, constant) *) let rec decompose_adds t: ((term * int) list) * int = - try ([], dest_small_numeral t) with _ -> + try ([], dest_small_numeral t) with Failure _ -> try let l,r = dest_binary "+" t in let lsyms,lconst = decompose_adds l in let rsyms,rconst = decompose_adds r in @@ -143,7 +143,7 @@ let rec MK_MEMORY_READ_EQ_BIGDIGIT_CONV = else map (fun (rsym,rcoeff) -> if rsym = lsym then (lsym,lcoeff + rcoeff) else (rsym,rcoeff)) rsyms) lsyms rsyms in - (syms,lconst+rconst) with _ -> + (syms,lconst+rconst) with Failure _ -> try (* note that num's subtraction is a bit complicated because num cannot be negative. However, there is a chance that even if the intermediate constants are negative the @@ -159,13 +159,13 @@ let rec MK_MEMORY_READ_EQ_BIGDIGIT_CONV = else map (fun (rsym,rcoeff) -> if rsym = lsym then (lsym,lcoeff - rcoeff) else (rsym,-rcoeff)) rsyms) lsyms rsyms in - (syms,lconst-rconst) with _ -> + (syms,lconst-rconst) with Failure _ -> try let l,r = dest_binary "*" t in let lconst = dest_small_numeral l in let rsyms,rconst = decompose_adds r in (map (fun (sym,coeff) -> (sym,coeff * lconst)) rsyms, rconst * lconst) - with _ -> ([t,1],0) + with Failure _ -> ([t,1],0) in let syms1,const1 = decompose_adds t1 in let syms2,const2 = decompose_adds t2 in @@ -233,7 +233,7 @@ let rec MK_MEMORY_READ_EQ_BIGDIGIT_CONV = (TAC_PROOF((assumptions,mk_eq(ptrofs,ptrofs')), IMP_REWRITE_TAC[WORD_SUB2] THEN SIMPLE_ARITH_TAC)) in get_base_ptr_and_ofs ptrofs' - with _ -> (ptr,ofs) + with Failure _ -> (ptr,ofs) in if not (is_multiple_of_8 ofs) then @@ -246,7 +246,7 @@ let rec MK_MEMORY_READ_EQ_BIGDIGIT_CONV = if constr_name = "bytes64" then let _ = assert (size = eight) in - let larger_reads = List.filter_map (fun (_,ath) -> + let larger_reads = filter_map (fun (_,ath) -> try let c = concl ath in if not (is_eq c) then None else @@ -271,12 +271,12 @@ let rec MK_MEMORY_READ_EQ_BIGDIGIT_CONV = not (ofs + 8 <= ofs2) | _ -> true end) then - Some (ath,Option.get c_access_info) + Some (ath,option_get c_access_info) else None end | _ -> None end - with _ -> + with Failure _ -> let _ = Printf.printf "Warning: MK_MEMORY_READ_EQ_BIGDIGIT_CONV: unexpected failure: `%s`\n" (string_of_term (concl ath))in None) assumptions in if larger_reads = [] @@ -285,7 +285,7 @@ let rec MK_MEMORY_READ_EQ_BIGDIGIT_CONV = Printf.printf "MK_MEMORY_READ_EQ_BIGDIGIT_CONV: found:\n"; List.iter (fun th,_ -> Printf.printf " `%s`\n" (string_of_term (concl th))) larger_reads)); - let extracted_reads = List.filter_map + let extracted_reads = filter_map (fun larger_read_th,(ptrofs2,(ptr2,ofs2),size2,_,_) -> try let larger_read = lhs (concl larger_read_th) in @@ -295,7 +295,7 @@ let rec MK_MEMORY_READ_EQ_BIGDIGIT_CONV = (string_of_term ofs2) in None else let ofsdiff = subtract_num ofs ofs2 in - let reldigitofs = Option.bind ofsdiff divide_by_8 in + let reldigitofs = option_bind ofsdiff divide_by_8 in let nwords = divide_by_8 size2 in begin match reldigitofs, nwords with @@ -328,7 +328,7 @@ let rec MK_MEMORY_READ_EQ_BIGDIGIT_CONV = (* strip word_add *) (AP_TERM_TAC THEN AP_TERM_TAC THEN SIMPLE_ARITH_TAC))) in Some (REWRITE_RULE[larger_read_th] eq_th,[]) - with _ -> + with Failure _ -> (if !equiv_print_log then Printf.printf "Could not prove `%s`\n" (string_of_term the_goal)); None end @@ -339,7 +339,7 @@ let rec MK_MEMORY_READ_EQ_BIGDIGIT_CONV = None end end - with _ -> begin + with Failure _ -> begin Printf.printf "Warning: MK_MEMORY_READ_EQ_BIGDIGIT_CONV: failed while processing `%s`\n" (string_of_term (concl larger_read_th)); None end) larger_reads in @@ -513,12 +513,12 @@ let DIGITIZE_MEMORY_READS th state_update_th = let th2',smaller_read_ths = MK_MEMORY_READ_EQ_BIGDIGIT_CONV the_rhs asl in let _ = new_memory_reads := th2'::(smaller_read_ths @ !new_memory_reads) in GEN_REWRITE_RULE RAND_CONV [th2'] th2 - with _ -> th2) (CONJUNCTS th) in + with Failure _ -> th2) (CONJUNCTS th) in (* new_memory_reads will still use the 'previous' state. update it. *) new_memory_reads := map (fun th -> try STATE_UPDATE_RULE ([NONOVERLAPPING_SIMPLE_64],[]) - state_update_th th with _ -> th) + state_update_th th with Failure _ -> th) !new_memory_reads; let res_th = end_itlist CONJ ths in @@ -529,7 +529,7 @@ let DIGITIZE_MEMORY_READS th state_update_th = Printf.printf "rewritten th: %s\n" (string_of_term (concl res_th)); Printf.printf "new_memory_reads th: %s\n" (if newmems_th = None then "None" else - ("Some " ^ (string_of_term (concl (Option.get newmems_th)))))) in + ("Some " ^ (string_of_term (concl (option_get newmems_th)))))) in res_th,newmems_th;; @@ -686,7 +686,7 @@ let ABBREV_READS_TAC (readth,readth2:thm*thm) (forget_expr:bool):tactic = Printf.printf "\t- Abbreviating `%s` as \"%s\" as well\n" (string_of_term rhs2) vname in (REWRITE_RULE[r] readth2),rhs - with _ -> + with Failure _ -> (* Inspect if this is the result of updating lower bits of the registers. *) (try @@ -699,7 +699,7 @@ let ABBREV_READS_TAC (readth,readth2:thm*thm) (forget_expr:bool):tactic = Printf.printf "\t- Abbreviating `%s` as \"%s\" instead\n" (string_of_term wlo2) vname in (REWRITE_RULE[r] readth2),wlo1 - with _ -> + with Failure _ -> Printf.printf "\t- Error: WORD_RULE could not prove `%s = %s`\n" (string_of_term rhs2) (string_of_term rhs); Printf.printf "If the two expressions seem semantically equivalent,"; @@ -786,7 +786,7 @@ let CLEAR_UNUSED_ABBREVS = (* assumptions that read states should not be removed *) alive_queue := i::!alive_queue else if is_eq (concl th) && is_var (rand (concl th)) && - not (String.ends_with ~suffix:"DO_NOT_CLEAR" asmname) then + not (ends_with "DO_NOT_CLEAR" asmname) then (* if th is 'e = var', mark it as initially dead & extract rhs var *) !asl_with_flags.(i) <- (false, (Some (rand (concl th)), asmname, th)) else @@ -1058,7 +1058,7 @@ let mk_equiv_statement_template let mk_bytes_loaded (s:term) (pc_var:term) (mc:term) (data:term option) = let _ = List.map2 type_check [s;pc_var;mc] [state_ty;`:num`;`:((8)word)list`] in let mc_all = if data = None then mc else - let data = Option.get data in + let data = option_get data in let _ = type_check data `:((8)word)list` in list_mk_icomb "APPEND" [mc;data] in @@ -1080,8 +1080,8 @@ let mk_equiv_statement_template let equiv_in_pred = fst (strip_comb (fst (dest_eq equiv_in_body))) in let equiv_out_pred = fst (strip_comb (fst (dest_eq equiv_out_body))) in - let data1_name = Option.map (fun x -> (lhs (concl x))) data1 in - let data2_name = Option.map (fun x -> (lhs (concl x))) data2 in + let data1_name = option_map (fun x -> (lhs (concl x))) data1 in + let data2_name = option_map (fun x -> (lhs (concl x))) data2 in let precond = mk_gabs (spair, (list_mk_conj [ mk_bytes_loaded s pc (lhs (concl mc1)) data1_name; @@ -1265,7 +1265,7 @@ let simplify_maychanges: term -> term = let SIMPLIFY_MAYCHANGES_TAC = W(fun (asl,w) -> - let mcs = List.filter_map + let mcs = filter_map (fun (_,asm) -> if maychange_term (concl asm) then Some asm else None) asl in MAP_EVERY (fun asm -> let x, st2 = dest_comb (concl asm) in diff --git a/common/for_hollight.ml b/common/for_hollight.ml index 37be09925..b63cc89a2 100644 --- a/common/for_hollight.ml +++ b/common/for_hollight.ml @@ -16,6 +16,42 @@ let rec dest_list = function let catch f x = try Some(f x) with Failure _ -> None;; +(* --------------------------------------------------------------------- *) +(* Compatibility shims for OCaml < 4.08 (Option module absent). *) +(* --------------------------------------------------------------------- *) + +let option_get = function Some x -> x | None -> failwith "option_get";; +let option_map f = function Some x -> Some (f x) | None -> None;; +let option_bind opt f = match opt with Some x -> f x | None -> None;; +let option_is_some = function Some _ -> true | None -> false;; + +(* --------------------------------------------------------------------- *) +(* Compatibility for List.filter_map (not available before OCaml 4.08). *) +(* --------------------------------------------------------------------- *) + +let rec filter_map f = function + | [] -> [] + | x :: xs -> + match f x with + | Some y -> y :: filter_map f xs + | None -> filter_map f xs;; + +(* --------------------------------------------------------------------- *) +(* Compatibility for String.starts_with/ends_with (OCaml < 4.13). *) +(* --------------------------------------------------------------------- *) + +let starts_with prefix s = + let plen = String.length prefix in + String.length s >= plen && String.sub s 0 plen = prefix;; + +let ends_with suffix s = + let slen = String.length suffix and len = String.length s in + len >= slen && String.sub s (len - slen) slen = suffix;; + +(* --------------------------------------------------------------------- *) +(* End of compatibility shims. *) +(* --------------------------------------------------------------------- *) + let rec takedrop (n:int) (l:'a list): 'a list * 'a list = if n = 0 then ([],l) else @@ -233,7 +269,7 @@ let BITMATCH_MEMO_CONV = begin try let ls, th' = inst_bitpat_numeral (hd (hyp th)) nn in PROVE_HYP th' (INST ls th) - with _ -> + with Failure _ -> failwith (sprintf "BITMATCH_MEMO_CONV: match failed: 0x%x" (Num.int_of_num nn)) end | _ -> failwith "BITMATCH_MEMO_CONV";; @@ -322,7 +358,7 @@ let conceal_bitmatch: term -> (thm * term * int * thm * conv) option = let ls, th' = inst_bitpat_numeral (hd (hyp th)) nn in (GEN_REWRITE_CONV I [new_abbrev] THENC GEN_REWRITE_CONV I [PROVE_HYP th' (INST ls th)]) tm - with _ -> + with Failure _ -> failwith (sprintf "conceal_bitmatch: match failed: 0x%x" n) end | _ -> failwith "" in diff --git a/common/misc.ml b/common/misc.ml index d14ca8c4d..a1ef11ae4 100644 --- a/common/misc.ml +++ b/common/misc.ml @@ -166,11 +166,14 @@ let CONS_TO_APPEND_CONV (t:term) = let elems = ref [] in let rec strip_cons (t:term):term = begin try - let the_cons,(itm::tail::[]) = strip_comb t in - if name_of the_cons <> "CONS" then failwith "" else - elems := itm::!elems; - strip_cons tail - with _ -> t + let the_cons,args = strip_comb t in + match args with + | [itm; tail] -> + if name_of the_cons <> "CONS" then failwith "" else + elems := itm::!elems; + strip_cons tail + | _ -> failwith "" + with Failure _ -> t end in let tail = strip_cons t in let new_list = mk_list (rev (!elems), type_of (hd !elems)) in @@ -2140,9 +2143,9 @@ let SAFE_UNIFY_REFL_TAC (allowed_vars_ref:term list ref) let used_vars = subtract lhs_vars allowed_vars in let used_vars = filter (fun v -> let n = name_of v in - forall (fun pfx -> not (String.starts_with ~prefix:pfx n)) + forall (fun pfx -> not (starts_with pfx n)) allowed_var_prefixes) used_vars in - if List.is_empty used_vars then + if used_vars = [] then UNIFY_REFL_TAC (asl,w) else (let diff = subtract lhs_vars allowed_vars in diff --git a/common/relational.ml b/common/relational.ml index 6270f6ff1..8f6ea400e 100644 --- a/common/relational.ml +++ b/common/relational.ml @@ -741,10 +741,10 @@ let ASSIGNS_SWAP_CONV tm = try let lref = assoc x !assigns_swap_conv_cache in try assoc y !lref - with _ -> + with Failure _ -> let newth = prove(the_goal,ASSIGNS_SWAP_TAC) in lref := (y, newth)::!lref; newth - with _ -> + with Failure _ -> let newth = prove(the_goal,ASSIGNS_SWAP_TAC) in assigns_swap_conv_cache := (x, ref [(y,newth)])::!assigns_swap_conv_cache; newth diff --git a/common/safety.ml b/common/safety.ml index 244e35e5e..89a623eb8 100644 --- a/common/safety.ml +++ b/common/safety.ml @@ -164,7 +164,7 @@ let safety_print_log = ref false;; stripping the exists f_events part. *) let ASSUME_CALLEE_SAFETY_TAC = let fresh_f_events_var_counter = ref 0 in - fun (callee_safety_proof:thm) (asmname:string) :tactic -> + fun (callee_safety_proof:thm) (asmname:string) -> let f_events_var_type = type_of (fst (dest_exists (concl callee_safety_proof))) in let f_events_callee = let _ = fresh_f_events_var_counter := 1 + !fresh_f_events_var_counter in diff --git a/tools/x86_safety_spec_generator.ml b/tools/x86_safety_spec_generator.ml index f8a0ee58c..66d2d3461 100644 --- a/tools/x86_safety_spec_generator.ml +++ b/tools/x86_safety_spec_generator.ml @@ -24,7 +24,7 @@ let mk_noibt_subroutine_safe_spec let ofs = find_term (fun t -> is_binary "word_sub" t && fst (dest_binary "word_sub" t) = stackptr) new_assum in Some (rand ofs) - with _ -> + with Failure _ -> let _ = Printf.printf "(* Has no \"word_sub stackpointer (word ..)\"; stackofs is None *)\n" in None in @@ -61,7 +61,7 @@ let mk_noibt_subroutine_safe_spec try let a,t' = dest_fun_ty t in let args,t0 = f t' in (a::args),t0 - with _ -> [],t in + with Failure _ -> [],t in let args,retty = f ty in let new_args = args @ (if already_has_stackptr then [type_of retaddr] diff --git a/x86/proofs/consttime.ml b/x86/proofs/consttime.ml index 2926b9de7..37b5074ee 100644 --- a/x86/proofs/consttime.ml +++ b/x86/proofs/consttime.ml @@ -47,7 +47,7 @@ let EXPAND_MAYCHANGE_YMM_REGS_TAC:tactic = try let lhs,rhs = dest_binary ",," t in (collect_maychange_components lhs) @ (collect_maychange_components rhs) - with _ -> + with Failure _ -> if is_comb t && name_of (rator t) = "MAYCHANGE" then let args = rand t in dest_list args @@ -60,12 +60,12 @@ let EXPAND_MAYCHANGE_YMM_REGS_TAC:tactic = let t,s = dest_comb t in let maychange_comps = collect_maychange_components t in (* map YMM to ZMM *) - let maychange_comps = List.map (fun t -> - try assoc t ymms with _ -> t) maychange_comps in + let maychange_comps = map (fun t -> + try assoc t ymms with Failure _ -> t) maychange_comps in (* unique it *) let maychange_comps = uniq (sort (<) maychange_comps) in - let new_maychanges = List.map (fun t -> + let new_maychanges = map (fun t -> let unary_list = mk_list ([t],type_of t) in mk_icomb (`MAYCHANGE`,unary_list)) maychange_comps in diff --git a/x86/proofs/decode.ml b/x86/proofs/decode.ml index e07be0270..3c022859f 100644 --- a/x86/proofs/decode.ml +++ b/x86/proofs/decode.ml @@ -1452,7 +1452,7 @@ let ADX_CONV = function | Comb(Const("adx",_),v) -> (try assoc v pths - with _ -> failwith "ADX_CONV") + with Failure _ -> failwith "ADX_CONV") | _ -> failwith "ADX_CONV";; let TO_WORDSIZE_CONV = @@ -1461,7 +1461,7 @@ let TO_WORDSIZE_CONV = function | Comb(Const("to_wordsize",_),v) -> (try assoc v pths - with _ -> failwith "TO_WORDSIZE_CONV") + with Failure _ -> failwith "TO_WORDSIZE_CONV") | _ -> failwith "TO_WORDSIZE_CONV";; let SIMD_TO_WORDSIZE_CONV = @@ -1470,7 +1470,7 @@ let SIMD_TO_WORDSIZE_CONV = function | Comb(Const("simd_to_wordsize",_),v) -> (try assoc v pths - with _ -> failwith "SIMD_TO_WORDSIZE_CONV") + with Failure _ -> failwith "SIMD_TO_WORDSIZE_CONV") | _ -> failwith "SIMD_TO_WORDSIZE_CONV";; let VEXL_SIZE_CONV = @@ -1479,7 +1479,7 @@ let VEXL_SIZE_CONV = function | Comb(Const("vexL_size",_),v) -> (try assoc v pths - with _ -> failwith "VEXL_SIZE_CONV") + with Failure _ -> failwith "VEXL_SIZE_CONV") | _ -> failwith "VEXL_SIZE_CONV";; let operand_of_RM = define diff --git a/x86/proofs/edwards25519_epadd.ml b/x86/proofs/edwards25519_epadd.ml index 6f877a843..486da42e6 100644 --- a/x86/proofs/edwards25519_epadd.ml +++ b/x86/proofs/edwards25519_epadd.ml @@ -2420,7 +2420,7 @@ let EDWARDS25519_EPADD_CORRECT = time prove MAP_EVERY X_GEN_TAC [`x1:int`; `y1:int`; `x2:int`; `y2:int`] THEN STRIP_TAC THEN EVERY_ASSUM(fun th -> try STRIP_ASSUME_TAC(MATCH_MP EDWARDS25519_EXPROJECTIVE_BOUND th) - with _ -> ALL_TAC) THEN + with Failure _ -> ALL_TAC) THEN DISCARD_STATE_TAC "s27" THEN DISCARD_MATCHING_ASSUMPTIONS [`aligned a b`; `nonoverlapping_modulo a b c`] THEN diff --git a/x86/proofs/edwards25519_epadd_alt.ml b/x86/proofs/edwards25519_epadd_alt.ml index d133e032b..e040578cd 100644 --- a/x86/proofs/edwards25519_epadd_alt.ml +++ b/x86/proofs/edwards25519_epadd_alt.ml @@ -2474,7 +2474,7 @@ let EDWARDS25519_EPADD_ALT_CORRECT = time prove MAP_EVERY X_GEN_TAC [`x1:int`; `y1:int`; `x2:int`; `y2:int`] THEN STRIP_TAC THEN EVERY_ASSUM(fun th -> try STRIP_ASSUME_TAC(MATCH_MP EDWARDS25519_EXPROJECTIVE_BOUND th) - with _ -> ALL_TAC) THEN + with Failure _ -> ALL_TAC) THEN DISCARD_STATE_TAC "s27" THEN DISCARD_MATCHING_ASSUMPTIONS [`aligned a b`; `nonoverlapping_modulo a b c`] THEN diff --git a/x86/proofs/equiv.ml b/x86/proofs/equiv.ml index 94a3c5768..f0f04235a 100644 --- a/x86/proofs/equiv.ml +++ b/x86/proofs/equiv.ml @@ -596,7 +596,7 @@ let X86_N_STEPS_AND_REWRITE_TAC execth (snums:int list) (inst_map: int list) if List.length abbrevs_for_st_n = List.length new_state_eqs then (* For each `read c sn = rhs`, replace rhs with abbrev *) - let new_state_eqs = List.filter_map + let new_state_eqs = filter_map (fun new_state_eq -> let rhs = rhs (concl new_state_eq) in (* Find 'rhs = abbrev' from the left program's updates. *) @@ -606,7 +606,7 @@ let X86_N_STEPS_AND_REWRITE_TAC execth (snums:int list) (inst_map: int list) | Some (_,rhs_to_abbrev) -> (try Some (GEN_REWRITE_RULE RAND_CONV [rhs_to_abbrev] new_state_eq) - with _ -> + with Failure _ -> (Printf.printf "Failed to proceed.\n"; Printf.printf "- rhs: `%s`\n" (string_of_term rhs); Printf.printf "- rhs_to_abbrev: `%s`\n" (string_of_thm rhs_to_abbrev); diff --git a/x86/proofs/mlkem_reduce.ml b/x86/proofs/mlkem_reduce.ml index 3c886ffbb..a084285ab 100644 --- a/x86/proofs/mlkem_reduce.ml +++ b/x86/proofs/mlkem_reduce.ml @@ -726,7 +726,7 @@ let MLKEM_REDUCE_NOIBT_WINDOWS_SUBROUTINE_SAFE = prove (* safety property version *) W(fun (asl,w) -> (* grab the current event list *) - let current_events = List.filter_map (fun (_,ath) -> let t = concl ath in + let current_events = filter_map (fun (_,ath) -> let t = concl ath in if is_eq t && is_read_events (lhs t) then Some (rhs t) else None) asl in if length current_events <> 1 diff --git a/x86/proofs/mlkem_tobytes.ml b/x86/proofs/mlkem_tobytes.ml index f6454e203..9c15bcca1 100644 --- a/x86/proofs/mlkem_tobytes.ml +++ b/x86/proofs/mlkem_tobytes.ml @@ -362,7 +362,7 @@ let MLKEM_TOBYTES_CORRECT = prove( REWRITE_TAC[bignum_of_wordlist; VAL] THEN POP_ASSUM_LIST (fun ths -> let dominated = filter (fun th -> - can (find_term (fun t -> try fst(dest_const t) = "bit" with _ -> false)) (concl th)) ths in + can (find_term (fun t -> try fst(dest_const t) = "bit" with Failure _ -> false)) (concl th)) ths in MAP_EVERY ASSUME_TAC (rev dominated)) THEN CONV_TAC(TOP_DEPTH_CONV DIMINDEX_CONV) THEN CONV_TAC(ONCE_DEPTH_CONV NUM_SUB_CONV) THEN diff --git a/x86/proofs/simulator.ml b/x86/proofs/simulator.ml index cee1fe1ad..004cd1f5e 100755 --- a/x86/proofs/simulator.ml +++ b/x86/proofs/simulator.ml @@ -894,8 +894,8 @@ let decode_inst ibytes = mk_flist(map (curry mk_comb `word:num->byte` o mk_small_numeral) ibytes) in let execth = X86_MK_EXEC_RULE(REFL ibyteterm) in let decoded = mk_flist - (map (rand o rand o snd o strip_forall o concl o Option.get) - (filter Option.is_some (Array.to_list (snd execth)))) in + (map (rand o rand o snd o strip_forall o concl o option_get) + (filter option_is_some (Array.to_list (snd execth)))) in let _ = print_term decoded in decoded;; @@ -960,10 +960,10 @@ let cosimulate_instructions (memopidx: int option) (add_assum: int) ibytes_list let execth = X86_MK_EXEC_RULE(REFL ibyteterm) in - let inst_th = Option.get (snd execth).(0) in + let inst_th = option_get (snd execth).(0) in let decoded = mk_flist - (map (rand o rand o snd o strip_forall o concl o Option.get) - (filter Option.is_some (Array.to_list (snd execth)))) in + (map (rand o rand o snd o strip_forall o concl o option_get) + (filter option_is_some (Array.to_list (snd execth)))) in let result = match diff --git a/x86/proofs/x86.ml b/x86/proofs/x86.ml index 9c800c8a3..8f5838bdd 100644 --- a/x86/proofs/x86.ml +++ b/x86/proofs/x86.ml @@ -4162,7 +4162,7 @@ let X86_THM = failwith ("X86_THM: Cannot decompose PC expression: " ^ string_of_term (concl pc_th)) in let _ = if !x86_print_log then - let opt = Option.get execth2.(pc_ofs) in + let opt = option_get execth2.(pc_ofs) in (* opt: |- forall ... bytes_loaded .. ==> x86_decode .. (INST ..) *) let t = snd (strip_forall (concl (opt))) in let t = snd (dest_imp t) in @@ -4173,7 +4173,7 @@ let X86_THM = CONV_RULE (ONCE_DEPTH_CONV (REWR_CONV (GSYM ADD_ASSOC) THENC RAND_CONV NUM_REDUCE_CONV)) - (MATCH_MP th (MATCH_MP (Option.get execth2.(pc_ofs)) loaded_mc_th));; + (MATCH_MP th (MATCH_MP (option_get execth2.(pc_ofs)) loaded_mc_th));; let X86_ENSURES_SUBLEMMA_TAC = ENSURES_SUBLEMMA_TAC o MATCH_MP bytes_loaded_update o CONJUNCT1;; @@ -4264,14 +4264,14 @@ let X86_CONV (decode_ths:thm option array) ths tm = (fun th -> let c = concl th in is_eq c && is_read_rip (fst (dest_eq c))) - ths with _ -> + ths with Failure _ -> failwith "X86_CONV: can't find `read RIP .. = ..` from ths" in (* Find `bytes_loaded ..`. *) let bytes_loaded_mc_ths:thm list = (* Pick the _mc const from decode_ths, if decode_ths[0] != None, which is likely to be true. *) - let the_mc:term option = Option.bind decode_ths.(0) + let the_mc:term option = option_bind decode_ths.(0) (fun th -> (* th is `forall .., bytes_loaded ... _mc ==> x86_decode ..`. *) let t = concl th in @@ -4285,11 +4285,11 @@ let X86_CONV (decode_ths:thm option array) ths tm = let cc = concl th in is_comb cc && ( let c,args = strip_comb (concl th) in c = bytes_loaded_tm && - (the_mc = None || last args = Option.get the_mc))) + (the_mc = None || last args = option_get the_mc))) ths in if res = [] then failwith ("X86_CONV: can't find `bytes_loaded .. .. " ^ - (if the_mc <> None then string_of_term (Option.get the_mc) else "..") + (if the_mc <> None then string_of_term (option_get the_mc) else "..") ^ "` from ths") else res in @@ -4299,8 +4299,8 @@ let X86_CONV (decode_ths:thm option array) ths tm = (* Pick the right rules. It will be a singleton in most cases... *) let x86_execute_case_rules:thm list = let ts = find_terms is_const (concl eth) in - List.filter_map (fun t -> - try Some ((assoc (name_of t) X86_EXECUTE_CASES)) with _ -> None) ts in + filter_map (fun t -> + try Some ((assoc (name_of t) X86_EXECUTE_CASES)) with Failure _ -> None) ts in (K eth THENC PURE_ONCE_REWRITE_CONV(x86_execute_case_rules) THENC REWRITE_CONV[add_store_event;add_load_event;SEQ_ID] THENC @@ -4689,7 +4689,7 @@ let X86_SUBROUTINE_SIM_TAC ?(is_safety_thm=false) and svar0 = mk_var("s",`:x86state`) in let ilist = map (vsubst[svar,svar0]) ilist0 in let subth_specl = - try SPECL ilist subth with _ -> begin + try SPECL ilist subth with Failure _ -> begin (if (!x86_print_log) then (Printf.printf "ilist and subth's forall vars do not match\n"; Printf.printf "ilist: [%s]\n" (end_itlist @@ -4844,7 +4844,7 @@ let check_forallvars_tac:tactic = let find_and_check (lhs_pat:term) (t:term) (quants:term list) = let read_eq = try Some (find_term (fun t -> is_eq t && can (term_match [] lhs_pat) (lhs t)) t) - with _ -> None in + with Failure _ -> None in match read_eq with | Some read_eq -> let the_var = rhs read_eq in @@ -5279,7 +5279,7 @@ let WINDOWS_X86_WRAP_STACK_TAC = let is_nargle t = is_comb t && rator t = argy in fun t -> try (length o dest_list o rand o find_term is_nargle) t - with _ -> failwith "Could not find WINDOWS_C_ARGUMENTS" in + with Failure _ -> failwith "Could not find WINDOWS_C_ARGUMENTS" in fun winmc stdmc coreth reglist stdstackoff (asl,w) -> let stdregs = dest_list reglist in let n = diff --git a/x86/tutorial/rel_equivtac.ml b/x86/tutorial/rel_equivtac.ml index 05bc5e9dc..27d5ad90c 100644 --- a/x86/tutorial/rel_equivtac.ml +++ b/x86/tutorial/rel_equivtac.ml @@ -254,7 +254,7 @@ let EXPAND_READ_XMM_SSE_RULE th = [read_ymm;`(128,128)`])) THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM th'] THEN CONV_TAC WORD_BLAST) - with _ -> failwith ("Could not expand " ^ (string_of_thm th));; + with Failure _ -> failwith ("Could not expand " ^ (string_of_thm th));; let org_extra_word_conv = !extra_word_CONV;;