jasminc: Add a -slice f command line argument

Slicing removes from a program functions and global variables that are
not reachable from the selected functions.

This feature has been requested in the context of safety checking: it
allows to analyze a single entry-point within a larger program.

Nonetheless it may be used for different purposes and in particular it
makes the already available `-checkCTon` and `-ec` arguments somehow
redundant.

CHANGELOG.md

@@ -55,6 +55,10 @@
   when the `-nocheckalignment` command-line flag is given
   ([PR #401](https://github.com/jasmin-lang/jasmin/pull/401)).
 
+- The `jasminc` tool may process only a slice of the input program, when
+  one or more `-slice f` arguments are given on the command line
+  ([PR #414](https://github.com/jasmin-lang/jasmin/pull/414)).
+
 ## Bug fixes
 
 - The x86 instructions `VMOVSHDUP` and `VMOVSLDUP` accept a size suffix (`_128`

compiler/src/glob_options.ml

@@ -10,6 +10,7 @@ let print_list = ref []
 let ecfile = ref ""
 let ec_list = ref []
 let ec_array_path = ref Filename.current_dir_name
+let slice = ref []
 let check_safety = ref false
 let safety_param = ref None
 let safety_config = ref None
@@ -67,6 +68,9 @@ let set_ec f =
 let set_ec_array_path p =
   ec_array_path := p
 
+let set_slice f =
+  slice := f :: !slice
+
 let set_constTime () = model := ConstantTime
 let set_safety () = model := Safety
 
@@ -168,6 +172,7 @@ let options = [
     "-checkCT", Arg.Unit set_ct         , ": checks that the full program is constant time (using a type system)";
     "-checkCTon", Arg.String set_ct_on  , "[f]: checks that the function [f] is constant time (using a type system)";
     "-infer"    , Arg.Set infer         , "infers security level annotations of the constant time type system";          
+    "-slice"    , Arg.String set_slice  , "[f]: keep function [f] and all what it needs";
     "-safety", Arg.Unit set_safety      , ": generates model for safety verification";
     "-checksafety", Arg.Unit set_checksafety, ": automatically check for safety";
     "-safetyparam", Arg.String set_safetyparam,

compiler/src/main_compiler.ml

@@ -150,6 +150,12 @@ let main () =
         hierror ~loc:(Lmore loc) ~kind:"typing error" "%s" code
     in
 
+    let prog =
+      if !slice <> []
+      then Slicing.slice !slice prog
+      else prog
+    in
+
     (* The source program, before any compilation pass. *)
     let source_prog = prog in
 

compiler/src/slicing.ml

@@ -0,0 +1,54 @@
+open Utils
+open Prog
+
+type keep = { vars : Sv.t; funs : Sf.t }
+
+let with_var k x = { k with vars = Sv.add x k.vars }
+let with_fun k f = { k with funs = Sf.add f k.funs }
+
+let inspect_gvar k { gs; gv } =
+  match gs with Slocal -> k | Sglob -> with_var k (L.unloc gv)
+
+let rec inspect_e k = function
+  | Pconst _ | Pbool _ | Parr_init _ -> k
+  | Pvar x -> inspect_gvar k x
+  | Pget (_, _, x, e) | Psub (_, _, _, x, e) -> inspect_gvar (inspect_e k e) x
+  | Pload (_, _, e) | Papp1 (_, e) -> inspect_e k e
+  | Papp2 (_, e1, e2) -> inspect_e (inspect_e k e1) e2
+  | PappN (_, es) -> inspect_es k es
+  | Pif (_, e1, e2, e3) -> inspect_e (inspect_e (inspect_e k e1) e2) e3
+
+and inspect_es k es = List.fold_left inspect_e k es
+
+let inspect_lv k = function
+  | Lnone _ | Lvar _ -> k
+  | Lmem (_, _, e) | Laset (_, _, _, e) | Lasub (_, _, _, _, e) -> inspect_e k e
+
+let inspect_lvs k xs = List.fold_left inspect_lv k xs
+
+let rec inspect_stmt k stmt = List.fold_left inspect_instr k stmt
+and inspect_instr k i = inspect_instr_r k i.i_desc
+
+and inspect_instr_r k = function
+  | Cassgn (x, _, _, e) -> inspect_lv (inspect_e k e) x
+  | Copn (xs, _, _, es) | Csyscall (xs, _, es) ->
+      inspect_lvs (inspect_es k es) xs
+  | Cif (g, a, b) | Cwhile (_, a, g, b) ->
+      inspect_stmt (inspect_stmt (inspect_e k g) a) b
+  | Cfor (_, (_, e1, e2), s) -> inspect_stmt (inspect_es k [ e1; e2 ]) s
+  | Ccall (_, xs, fn, es) -> with_fun (inspect_lvs (inspect_es k es) xs) fn
+
+let slice fs (gd, fds) =
+  let k =
+    List.fold_left
+      (fun k fd ->
+        let n = fd.f_name in
+        if Sf.mem n k.funs then inspect_stmt k fd.f_body
+        else if List.exists (String.equal n.fn_name) fs then
+          inspect_stmt (with_fun k n) fd.f_body
+        else k)
+      { vars = Sv.empty; funs = Sf.empty }
+      fds
+  in
+  ( List.filter (fun (x, _) -> Sv.mem x k.vars) gd,
+    List.filter (fun fd -> Sf.mem fd.f_name k.funs) fds )

compiler/src/slicing.mli

@@ -0,0 +1,2 @@
+open Prog
+val slice : string list -> ('a, 'b) prog -> ('a, 'b) prog