Drop legacy interface to the safety checker

.gitlab-ci.yml

@@ -83,7 +83,7 @@ coq-master:
 ocaml:
   stage: build
   variables:
-    EXTRA_NIX_ARGUMENTS: --arg ocamlDeps true
+    EXTRA_NIX_ARGUMENTS: --arg ocamlDeps true --arg safetyDeps true
   extends: .common
   needs:
   - coq-program
@@ -165,7 +165,7 @@ opam-from-tarball:
 check:
   stage: test
   variables:
-    EXTRA_NIX_ARGUMENTS: --arg testDeps true --arg ocamlDeps true
+    EXTRA_NIX_ARGUMENTS: --arg testDeps true --arg ocamlDeps true --arg safetyDeps true
   extends: .common
   needs:
   - coq-program
@@ -221,7 +221,7 @@ libjade:
     matrix:
       - PRIMITIVE: [ mldsa, mlkem, xmss ]
   variables:
-    EXTRA_NIX_ARGUMENTS: --arg ocamlDeps true
+    EXTRA_NIX_ARGUMENTS: --arg testDeps true
   extends: .common
   needs:
   - coq-program

changes/03-other/1472-exit-legacy-checksafety.md

@@ -0,0 +1,3 @@
+- The deprecated legacy CLI interface (`jasminc`) to the safety checker has
+  been removed
+  ([PR 1472](https://github.com/jasmin-lang/jasmin/pull/1472)).

compiler/src/CLI_errors.ml

@@ -62,13 +62,4 @@ let check_options () =
     then warning Experimental Location.i_dummy
       "support of the RISC-V architecture is experimental";
 
-  if
-    !check_safety || !trust_aligned || !safety_param <> None
-    || !safety_config <> None
-    || !safety_makeconfigdoc <> None
-  then
-    warning Deprecated Location.i_dummy
-      "the legacy (jasminc) interface to the safety checker is deprecated; use \
-       jasmin-checksafety instead";
-
   chk_out_file outfile

compiler/src/dune

@@ -21,4 +21,4 @@
 (library
  (name jasminc)
  (modules main_compiler)
- (libraries jasmin jasmin_checksafety linter))
+ (libraries jasmin linter))

compiler/src/glob_options.ml

@@ -9,11 +9,7 @@ let timings = ref false
 let print_list = ref []
 let print_liveness = ref false
 let slice = ref []
-let check_safety = ref false
-let safety_param = ref None
-let safety_config = ref None
 let stop_after = ref None
-let safety_makeconfigdoc = ref None   
 let trust_aligned = ref false
 
 let help_version = ref false
@@ -96,11 +92,6 @@ let set_all_print () =
 let set_slice f =
   slice := f :: !slice
 
-let set_checksafety () = check_safety := true
-let set_safetyparam s = safety_param := Some s
-let set_safetyconfig s = safety_config := Some s
-let set_safety_makeconfigdoc s = safety_makeconfigdoc := Some s
-
 let set_color c =
   let assoc = function
     | "auto"   -> Auto
@@ -202,17 +193,6 @@ let options = [
     "-set0"     , Arg.Set set0          , " Use [xor x x] to set x to 0 (default is not)";
     "-noset0"   , Arg.Clear set0        , " Do not use set0 option";
     "-slice"    , Arg.String set_slice  , "[f] Keep function [f] and everything it needs";
-    "-checksafety", Arg.Unit set_checksafety, " Automatically check for safety (deprecated)";
-    "-safetyparam", Arg.String set_safetyparam,
-    " Parameter for automatic safety verification:\n    \
-     format: \"f_1>param_1|f_2>param_2|...\" \
-     where each param_i is of the form:\n    \
-     pt_1,...,pt_n;len_1,...,len_k\n    \
-     pt_1,...,pt_n: input pointers of f_i\n    \
-     len_1,...,len_k: input lengths of f_i\n    (deprecated)";
-     "-safetyconfig", Arg.String set_safetyconfig, "[filename] Use filename (JSON) as configuration file for the safety checker (deprecated)";
-    "-safetymakeconfigdoc", Arg.String set_safety_makeconfigdoc, "[dir] Make the safety checker configuration docs in [dir] (deprecated)";
-    "-nocheckalignment", Arg.Set trust_aligned, " Do not report alignment issue as safety violations (deprecated)";
     "-wlea", Arg.Unit (add_warning UseLea), " Print warning when lea is used";
     "-wea", Arg.Unit (add_warning ExtraAssignment), " Print warning when extra assignment is introduced";
     "-winsertarraycopy", Arg.Unit (add_warning IntroduceArrayCopy), " Print warning when array copy is introduced";

compiler/src/main_compiler.ml

@@ -1,5 +1,4 @@
 open Jasmin
-open Jasmin_checksafety
 open Utils
 open Prog
 open Glob_options
@@ -25,7 +24,7 @@ let parse () =
   if c then enable_colors ();
   match !infiles with
   | [] ->
-    if !help_intrinsics || !safety_makeconfigdoc <> None || !help_version
+    if !help_intrinsics || !help_version
     then ""
     else error()
   | [ infile ] ->
@@ -34,56 +33,20 @@ let parse () =
     infile
   | infile :: s :: _ -> raise CLI_errors.(CLIerror (RedundantInputFile (infile, s)))
 
-(* -------------------------------------------------------------------- *)
-let check_safety_p pd msf_size asmOp analyze s (p : (_, 'asm) Prog.prog) =
-  let () = if SafetyConfig.sc_print_program () then
-      let s1,s2 = Glob_options.print_strings s in
-      Format.eprintf "@[<v>At compilation pass: %s@;%s@;@;\
-                      %a@;@]@."
-        s1 s2
-        (Printer.pp_prog ~debug:true pd msf_size asmOp) p
-  in
-
-  let () = SafetyConfig.pp_current_config_diff () in
-
-  let is_safe =
-    List.fold_left (fun res f_decl ->
-        if FInfo.is_export f_decl.f_cc then
-          let () = Format.eprintf "@[<v>Analyzing function %s@]@."
-              f_decl.f_name.fn_name in
-
-          analyze ?fmt:None ~safety_param:!Glob_options.safety_param f_decl p && res
-        else res)
-      true
-      (List.rev (snd p)) in
-  if not is_safe then exit(2)
-
 (* -------------------------------------------------------------------- *)
 let main () =
 
   try
     let infile = parse() in
 
-    let (module P) = SafetyMain.get_arch_with_analyze !target_arch !call_conv in
-    let module Arch = P.A in
-
-    if !safety_makeconfigdoc <> None
-    then (
-      let dir = oget !safety_makeconfigdoc in
-      SafetyConfig.mk_config_doc dir;
-      exit 0);
+    let (module Arch) = CoreArchFactory.get_arch_module !target_arch !call_conv in
 
     if !help_intrinsics
     then (Help.show_intrinsics Arch.asmOp_sopn (); exit 0);
 
     if !help_version
     then (Format.printf "%s@." version_string; exit 0);
 
-    let () = if !check_safety then
-        match !safety_config with
-        | Some conf -> SafetyConfig.load_config conf
-        | None -> () in
-
     let env, pprog, _ast =
       try Compile.parse_file Arch.arch_info ~idirs:!Glob_options.idirs infile
       with
@@ -140,21 +103,10 @@ let main () =
     end;
 
     (* This function is called after each compilation pass.
-        - Check program safety (and exit) if the time has come
         - Pretty-print the program
         - Add your own checker here!
     *)
     let visit_prog_after_pass ~debug s p =
-      if s = SafetyConfig.sc_comp_pass () && !check_safety then
-        check_safety_p
-          Arch.pointer_data
-          Arch.msf_size
-          Arch.asmOp
-          P.analyze
-          s
-          p
-        |> fun () -> exit 0
-      else
         eprint s (Printer.pp_prog ~debug Arch.pointer_data Arch.msf_size Arch.asmOp) p
     in
 

default.nix

@@ -4,6 +4,7 @@
 , coqDeps ? !inCI
 , coqMaster ? false
 , ocamlDeps ? !inCI
+, safetyDeps ? !inCI
 , testDeps ? !inCI
 , devTools ? !inCI
 , ecRef ? ""
@@ -85,13 +86,15 @@ stdenv.mkDerivation {
       mathcomp-word
       coqPackages.ITree
     ]
-    ++ optionals testDeps ([ curl.bin oP.apron.out llvmPackages.bintools-unwrapped ] ++ (with python3Packages; [ python pyyaml ]))
-    ++ optionals ocamlDeps ([ mpfr ppl ] ++ (with oP; [
+    ++ optionals testDeps ([ curl.bin gmp llvmPackages.bintools-unwrapped ] ++ (with python3Packages; [ python pyyaml ]))
+    ++ optionals (testDeps && safetyDeps) [ oP.apron.out ]
+    ++ optionals ocamlDeps (with oP; [
          ocaml findlib dune_3
          cmdliner
          angstrom
          batteries
-         menhir (oP.menhirLib or null) zarith camlidl apron yojson ]))
+         menhir oP.menhirLib zarith yojson ])
+    ++ optionals (ocamlDeps && safetyDeps) ([ mpfr ppl ] ++ (with oP; [ camlidl apron ]))
     ++ optionals devTools (with oP; [ merlin ocaml-lsp ])
     ++ optionals ecDeps [ easycrypt z3.out ]
     ++ optionals opamDeps [ rsync git pkg-config perl ppl mpfr opam ]