3d: make --makefile honor --save_hashes

src/3d/Batch.fsti

@@ -87,3 +87,9 @@ val check_all_hashes
   (out_dir: string)
   (files_and_modules: list (string & string))
 : ML unit
+
+val save_hashes_for_module
+  (out_dir: string)
+  (file: string)
+  (modul: string)
+: ML unit

src/3d/GenMakefile.fst

@@ -528,6 +528,33 @@ let produce_everparse_h_rule
     }
   ] else []
 
+let produce_hash_rule
+  (g: Deps.dep_graph)
+  (file: string)
+: FStar.All.ML rule_t
+=
+  let modul = Options.get_module_name file in
+  let deps =
+    [mk_input_filename file;
+     mk_filename modul "c";
+     mk_filename modul "h"]
+    `List.Tot.append`
+    (if Deps.has_entrypoint g modul
+     then [mk_filename (Printf.sprintf "%sWrapper" modul) "c";
+           mk_filename (Printf.sprintf "%sWrapper" modul) "h"]
+     else [])
+    `List.Tot.append`
+    (if Deps.has_static_assertions g modul
+     then [mk_filename (Printf.sprintf "%sStaticAssertions" modul) "c"]
+     else [])
+  in
+  {
+    ty = EverParse;
+    from = deps;
+    to = mk_filename modul "json";
+    args = Printf.sprintf "--__micro_step save_hashes %s" (mk_input_filename file);
+  }
+
 noeq
 type produce_makefile_res = {
   rules: list rule_t;
@@ -542,6 +569,7 @@ let produce_makefile
   (skip_o_rules: bool)
   (clang_format: bool)
   (copy_clang_format_opt: bool)
+  (save_hashes: bool)
   (files: list string)
 : FStar.All.ML produce_makefile_res
 =
@@ -566,7 +594,8 @@ let produce_makefile
     List.Tot.concatMap (produce_external_api_krml_rule g) all_modules `List.Tot.append`
     List.map (produce_krml_rule g) all_modules `List.Tot.append`
     List.concatMap (produce_h_rules g clang_format) all_files `List.Tot.append`
-    produce_config_fst_file_rule ()
+    produce_config_fst_file_rule () `List.Tot.append`
+    (if save_hashes then List.map (produce_hash_rule g) all_files else [])
   in {
     graph = g;
     rules = rules;
@@ -581,13 +610,14 @@ let write_makefile
   (skip_o_rules: bool)
   (clang_format: bool)
   (copy_clang_format_opt: bool)
+  (save_hashes: bool)
   (files: list string)
 : FStar.All.ML unit
 =
   let makefile_final = Options.get_makefile_name () in
   let makefile_tmp = makefile_final ^ ".tmp" in
   let file = FStar.IO.open_write_file makefile_tmp in
-  let {graph = g; rules; all_files} = produce_makefile mtype everparse_h emit_output_types_defs skip_o_rules clang_format copy_clang_format_opt files in
+  let {graph = g; rules; all_files} = produce_makefile mtype everparse_h emit_output_types_defs skip_o_rules clang_format copy_clang_format_opt save_hashes files in
   FStar.IO.write_string file (String.concat "" (List.Tot.map (print_make_rule mtype everparse_h input_stream_binding) rules));
   let write_all_ext_files (ext_cap: string) (ext: string) : FStar.All.ML unit =
     let ln =
@@ -621,5 +651,9 @@ let write_makefile
   write_all_ext_files "H" "h";
   write_all_ext_files "C" "c";
   write_all_ext_files "O" (oext mtype);
+  if save_hashes then begin
+    let json_files = List.map (fun f -> mk_filename (Options.get_module_name f) "json") all_files in
+    FStar.IO.write_string file (Printf.sprintf "EVERPARSE_ALL_JSON_FILES=%s\n" (String.concat " " (List.Tot.map (mk_rule_operand mtype) json_files)))
+  end;
   FStar.IO.close_write_file file;
   OS.rename makefile_tmp makefile_final

src/3d/GenMakefile.fsti

@@ -8,5 +8,6 @@ val write_makefile
   (skip_o_rules: bool)
   (clang_format: bool)
   (copy_clang_format_opt: bool)
+  (save_hashes: bool)
   (files: list string)
 : FStar.All.ML unit

src/3d/HashingOptions.fst

@@ -13,6 +13,7 @@ type micro_step_t =
   | MicroStepCopyClangFormat
   | MicroStepCopyEverParseH
   | MicroStepEmitConfig
+  | MicroStepSaveHashes
 
 type makefile_type =
   | MakefileGMake

src/3d/Main.fst

@@ -713,6 +713,16 @@ let go () : ML unit =
     in
     exit 0
   else
+  if micro_step = Some HashingOptions.MicroStepSaveHashes
+  then
+  (* Special mode: --__micro_step save_hashes *)
+    let out_dir = Options.get_output_dir () in
+    let _ = OS.mkdir out_dir in
+    List.iter (fun file ->
+      Batch.save_hashes_for_module out_dir file (Options.get_module_name file)
+    ) cmd_line_files;
+    exit 0
+  else
   (* for other modes, a nonempty list of files is needed on the command line, so if none are there, then we shall print the help message *)
   let input_stream_binding = Options.get_input_stream_binding () in
   if Nil? cmd_line_files
@@ -740,6 +750,7 @@ let go () : ML unit =
       (Options.get_skip_o_rules ())
       (Options.get_clang_format ())
       (not (Options.get_clang_format_use_custom_config ()))
+      (Options.get_save_hashes ())
       cmd_line_files
   | None ->
   (* Special mode: --__produce_c_from_existing_krml *)

src/3d/Options.fst

@@ -50,6 +50,7 @@ let valid_micro_step (str: string) : Tot bool = match str with
   | "copy_clang_format"
   | "copy_everparse_h"
   | "emit_config"
+  | "save_hashes"
     -> true
   | _ -> false
 let micro_step : ref (option (valid_string valid_micro_step)) = alloc None
@@ -389,7 +390,7 @@ let (display_usage_2, compute_options_2, fstar_options) =
     CmdOption "z3_use_ptr" (OptBool use_ptr_for_probe) "use pointers rather than array indices for probes" [];
     CmdOption "z3_witnesses" (OptStringOption "nb" always_valid z3_witnesses) "ask for nb distinct test witnesses per branch case (default 1)" [];
     CmdOption "__arg0" (OptStringOption "executable name" always_valid arg0) "executable name to use for the help message" [];
-    CmdOption "__micro_step" (OptStringOption "verify|extract|copy_clang_format|copy_everparse_h|emit_config" valid_micro_step micro_step) "micro step" [];
+    CmdOption "__micro_step" (OptStringOption "verify|extract|copy_clang_format|copy_everparse_h|emit_config|save_hashes" valid_micro_step micro_step) "micro step" [];
     CmdOption "__produce_c_from_existing_krml" (OptBool produce_c_from_existing_krml) "produce C from .krml files" [];
     CmdOption "__skip_deps" (OptBool skip_deps) "skip dependency analysis, assume all dependencies are specified on the command line" [];
   ];
@@ -489,6 +490,7 @@ let get_micro_step _ =
   | Some "copy_clang_format" -> Some MicroStepCopyClangFormat
   | Some "copy_everparse_h" -> Some MicroStepCopyEverParseH
   | Some "emit_config" -> Some MicroStepEmitConfig
+  | Some "save_hashes" -> Some MicroStepSaveHashes
 
 let get_produce_c_from_existing_krml _ =
   !produce_c_from_existing_krml

src/3d/ocaml/Batch.ml

@@ -731,6 +731,12 @@ let save_hashes
     let json = filename_concat out_dir (Printf.sprintf "%s.json" modul) in
     Hashing.save_hashes file (Some c) json
 
+let save_hashes_for_module
+      (out_dir: string)
+      (file: string)
+      (modul: string)
+  = save_hashes out_dir (file, modul)
+
 (* Copy .clang-format *)
 
 let copy_clang_format out_dir =

src/3d/tests/Makefile

@@ -42,7 +42,7 @@ OTHER_HEADERS=TestFieldPtrBase.h AlignC.h
 all: batch-test batch-test-negative batch-cleanup-test inplace-hash-test modules \
 	 tcpip extern output-types batch-interpret-test elf-test static funptr ifdefs \
 	 probe iter z3-testgen-test exttype z3-testgen-probe-test specialize_test specialize_test2 \
-	 specialize_tagged_union_array
+	 specialize_tagged_union_array save_hashes
 
 .PHONY: exttype
 
@@ -95,6 +95,10 @@ specialize_test2:
 specialize_tagged_union_array:
 	+$(MAKE) -C $@
 
+.PHONY: save_hashes
+save_hashes:
+	+$(MAKE) -C $@
+
 batch-test-negative: $(addsuffix .negtest,$(wildcard FAIL*.3d))
 
 %.3d.negtest: %.3d
@@ -167,6 +171,6 @@ clean-files:
 
 .PHONY: clean-files
 
-clean: clean-files specialize_test.clean specialize_test2.clean probe.clean extern.clean exttype.clean funptr.clean ifdefs.clean iter/coarse.clean iter/fine.clean modules.clean output_types.clean static.clean tcpip.clean specialize_tagged_union_array.clean
+clean: clean-files specialize_test.clean specialize_test2.clean probe.clean extern.clean exttype.clean funptr.clean ifdefs.clean iter/coarse.clean iter/fine.clean modules.clean output_types.clean static.clean tcpip.clean specialize_tagged_union_array.clean save_hashes.clean
 
 .PHONY: all batch-test batch-test-negative %.negtest clean batch-cleanup-test inplace-hash-test modules tcpip extern %.interpret batch-interpret-test static funptr ifdefs

src/3d/tests/save_hashes/.gitignore

@@ -0,0 +1 @@
+obj/

src/3d/tests/save_hashes/Makefile

@@ -0,0 +1,39 @@
+# Test that --save_hashes is honored with --makefile.
+# The generated Makefile should produce .json hash files,
+# and --check_hashes strong should validate them.
+
+all: check
+
+EVERPARSE_HOME ?= $(realpath ../../../..)
+export EVERPARSE_HOME
+
+FSTAR_EXE ?= fstar.exe
+EVERPARSE_CMD=$(EVERPARSE_HOME)/bin/3d.exe --fstar $(FSTAR_EXE)
+
+EVERPARSE_OUTPUT_DIR=obj
+EVERPARSE_INPUT_DIR=src
+
+everparse_makefile=$(EVERPARSE_OUTPUT_DIR)/EverParse.Makefile
+
+$(EVERPARSE_OUTPUT_DIR):
+	mkdir -p $@
+
+# Generate the Makefile with --save_hashes
+$(everparse_makefile): $(wildcard src/*.3d) | $(EVERPARSE_OUTPUT_DIR)
+	$(EVERPARSE_CMD) --makefile gmake --save_hashes --skip_o_rules --no_copy_everparse_h --makefile_name $@ src/Test.3d src/Test2.3d
+
+ifeq (,$(filter clean,$(MAKECMDGOALS)))
+include $(everparse_makefile)
+endif
+
+# Build all generated files including hash .json files
+build: $(EVERPARSE_ALL_H_FILES) $(EVERPARSE_ALL_C_FILES) $(EVERPARSE_ALL_JSON_FILES)
+
+# Verify saved hashes with --check_hashes strong
+check: build
+	$(EVERPARSE_CMD) --odir $(EVERPARSE_OUTPUT_DIR) --check_hashes strong src/Test.3d src/Test2.3d
+
+clean:
+	rm -rf $(EVERPARSE_OUTPUT_DIR)
+
+.PHONY: all build check clean

src/3d/tests/save_hashes/src/Test.3d

@@ -0,0 +1,6 @@
+entrypoint
+typedef struct _Pair
+{
+  UINT32 fst;
+  UINT32 snd;
+} Pair;

src/3d/tests/save_hashes/src/Test2.3d

@@ -0,0 +1,7 @@
+entrypoint
+typedef struct _Triple
+{
+  UINT32 x;
+  UINT32 y;
+  UINT32 z;
+} Triple;