jazzct: add --doit argument

Co-authored-by:  Ján Jančár <johny@neuromancer.sk>

compiler/CCT/fail/doit/x86_64/rol.jazz

@@ -0,0 +1,6 @@
+// This is CT in the ordinary sense, but not DOIT as ROL is not DOIT.
+export fn rol(#secret reg u32 x) -> #secret reg u32 {
+  x <<r = 5;
+  x = x;
+  return x;
+}

compiler/CCT/fail/doit/x86_64/xchg.jazz

@@ -0,0 +1,7 @@
+// This is CT in the ordinary sense, but not DOIT as XCHG is not DOIT.
+export fn xchange(#secret reg u32 a, #secret reg u32 b) -> #secret reg u32, #secret reg u32 {
+    a = a;
+    b = b;
+    a, b = #swap(a, b);
+    return a, b;
+}

compiler/Makefile

@@ -7,7 +7,7 @@ CHECK     := $(CHECKPY) scripts/runtest --jobs="$(JSJOBS)"
 CHECK     += config/tests.config
 CHECKCATS ?= \
 	safety \
-	CCT \
+	CCT CCT-DOIT \
 	x86-64-ATT \
 	x86-64-Intel \
 	x86-64-print \

compiler/config/tests.config

@@ -14,6 +14,12 @@ kodirs = !safety/fail
 bin    = ./scripts/check-cct
 okdirs = !CCT/success
 kodirs = !CCT/fail
+exclude = !CCT/**/doit
+
+[test-CCT-DOIT]
+bin    = ./scripts/check-cct
+args = --doit
+kodirs = !CCT/fail/doit
 
 [test-SCT]
 bin    = ./scripts/check-cct

compiler/entry/jazzct.ml

@@ -5,7 +5,7 @@ open Utils
 
 let parse_and_check arch call_conv =
   let module A = (val get_arch_module arch call_conv) in
-  let check infer ct_list speculative pass file =
+  let check ~doit infer ct_list speculative pass file =
     let _env, pprog, _ast =
       try Compile.parse_file A.arch_info file with
       | Annot.AnnotationError (loc, code) ->
@@ -44,7 +44,7 @@ let parse_and_check arch call_conv =
     in
 
     if speculative then
-      match Sct_checker_forward.ty_prog A.is_ct_sopn prog ct_list with
+      match Sct_checker_forward.ty_prog (A.is_ct_sopn ~doit) prog ct_list with
       | exception Annot.AnnotationError (loc, code) ->
           hierror ~loc:(Lone loc) ~kind:"annotation error" "%t" code
       | sigs ->
@@ -53,7 +53,7 @@ let parse_and_check arch call_conv =
             sigs
     else
       let sigs, errs =
-        Ct_checker_forward.ty_prog A.is_ct_sopn ~infer prog ct_list
+        Ct_checker_forward.ty_prog (A.is_ct_sopn ~doit) ~infer prog ct_list
       in
       Format.printf "/* Security types:\n@[<v>%a@]*/@."
         (pp_list "@ " (Ct_checker_forward.pp_signature prog))
@@ -63,8 +63,13 @@ let parse_and_check arch call_conv =
       in
       Stdlib.Option.iter on_err errs
   in
-  fun infer ct_list speculative compile file ->
-    match check infer ct_list speculative compile file with
+  fun infer ct_list speculative compile file doit ->
+    let compile =
+      if doit && compile < Compiler.PropagateInline then
+        Compiler.PropagateInline
+      else compile
+    in
+    match check ~doit infer ct_list speculative compile file with
     | () -> ()
     | exception HiError e ->
         Format.eprintf "%a@." pp_hierror e;
@@ -104,6 +109,10 @@ let file =
   let doc = "The Jasmin source file to verify" in
   Arg.(required & pos 0 (some non_dir_file) None & info [] ~docv:"JAZZ" ~doc)
 
+let doit =
+  let doc = "Allow only DOIT instructions on secrets" in
+  Arg.(value & flag & info [ "doit" ] ~doc)
+
 let () =
   let doc = "Check Constant-Time security of Jasmin programs" in
   let man =
@@ -118,5 +127,5 @@ let () =
   Cmd.v info
     Term.(
       const parse_and_check $ arch $ call_conv $ infer $ slice $ speculative
-      $ compile $ file)
+      $ compile $ file $ doit)
   |> Cmd.eval |> exit