From bb1df2b3bd67e592042e002fa4941c119d96787d Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Wed, 25 Oct 2023 14:24:55 -0700
Subject: [PATCH] test checker: define error handler to report errors

---
 src/3d/Target.fst    | 16 ++++++++++------
 src/3d/Target.fsti   |  1 +
 src/3d/Z3TestGen.fst | 40 ++++++++++++++++++++++++++++++++++------
 3 files changed, 45 insertions(+), 12 deletions(-)

diff --git a/src/3d/Target.fst b/src/3d/Target.fst
index fa6682359..344b0b624 100644
--- a/src/3d/Target.fst
+++ b/src/3d/Target.fst
@@ -1118,6 +1118,15 @@ let wrapper_name
     fn
   |> pascal_case
 
+let validator_name
+  (modul: string)
+  (fn: string)
+: ML string
+= Printf.sprintf "%s_validate_%s"
+    modul
+    fn
+  |> pascal_case
+
 let print_c_entry
                   (produce_everparse_error: opt_produce_everparse_error)
                   (modul: string)
@@ -1236,12 +1245,7 @@ let print_c_entry
              wrapper_name
              (print_params params)
     in
-    let validator_name =
-       Printf.sprintf "%s_validate_%s"
-         modul
-         d.decl_name.td_name.A.v.A.name
-       |> pascal_case
-    in
+    let validator_name = validator_name modul d.decl_name.td_name.A.v.A.name in
     let impl =
       let body = 
         if is_input_stream_buffer
diff --git a/src/3d/Target.fsti b/src/3d/Target.fsti
index 7bf907163..3a0db0439 100644
--- a/src/3d/Target.fsti
+++ b/src/3d/Target.fsti
@@ -421,6 +421,7 @@ val print_decls (modul: string) (ds:list decl) : ML string
 val print_types_decls (modul: string) (ds:list decl) : ML string
 val print_decls_signature (modul: string) (ds:list decl) : ML string
 val wrapper_name (modul: string) (fn: string) : ML string
+val validator_name (modul: string) (fn: string) : ML string
 type produce_everparse_error = | ProduceEverParseError
 type opt_produce_everparse_error = option produce_everparse_error
 val print_c_entry (_: opt_produce_everparse_error) (modul: string) (env: global_env) (ds:list decl)
diff --git a/src/3d/Z3TestGen.fst b/src/3d/Z3TestGen.fst
index 43b51671f..7d972c624 100644
--- a/src/3d/Z3TestGen.fst
+++ b/src/3d/Z3TestGen.fst
@@ -871,6 +871,13 @@ let module_and_wrapper_name
   | [modul; fn] -> modul, Target.wrapper_name modul fn
   | _ -> failwith "Z3TestGen.wrapper_name"
 
+let module_and_validator_name
+  (s: string)
+: ML (string & string)
+= match String.split ['.'] s with
+  | [modul; fn] -> modul, Target.validator_name modul fn
+  | _ -> failwith "Z3TestGen.validator_name"
+
 let rec print_witness_args_as_c
   (out: (string -> ML unit))
   (l: list arg_type) (args: list string)
@@ -1197,7 +1204,7 @@ unsigned long long "^arg_var^" = 0;
 
 let test_checker_c
   (modul: string)
-  (wrapper_name: string)
+  (validator_name: string)
   (params: list arg_type)
 : Tot string
 =
@@ -1205,13 +1212,33 @@ let test_checker_c
   let nb_cmd_and_args_s = string_of_int nb_cmd_and_args in
   let nb_args_s = string_of_int (nb_cmd_and_args - 1) in
   "
-#include \""^modul^"Wrapper.h\"
+#include \""^modul^".h\"
 #include <fcntl.h>
 #include <sys/mman.h>
 #include <sys/stat.h>
 #include <stdint.h>
 #include <unistd.h>
 #include <stdlib.h>
+
+static void TestErrorHandler (
+  const char *typename_s,
+  const char *fieldname,
+  const char *reason,
+  uint64_t error_code,
+  uint8_t *context,
+  EVERPARSE_INPUT_BUFFER input,
+  uint64_t start_pos
+) {
+  (void) error_code;
+  (void) input;
+  if (*context) {
+    printf(\"Reached from position %ld: type name %s, field name %s\\n\", start_pos, typename_s, fieldname);
+  } else {
+    printf(\"Parsing failed at position %ld: type name %s, field name %s. Reason: %s\\n\", start_pos, typename_s, fieldname, reason);
+    *context = 1;
+  }
+}
+
 int main(int argc, char** argv) {
   if (argc < "^nb_cmd_and_args_s^") {
     printf(\"Wrong number of arguments, expected "^nb_args_s^", got %d\\n\", argc);
@@ -1244,10 +1271,11 @@ int main(int argc, char** argv) {
   }
   uint8_t * buf = (uint8_t *) vbuf;
   printf(\"Read %ld bytes from %s\\n\", len, filename);
-  BOOLEAN result = "^wrapper_name^"("^call_args_lhs^"buf, len);
+  uint8_t context = 0;
+  uint64_t result = "^validator_name^"("^call_args_lhs^"&context, &TestErrorHandler, buf, len, 0);
   munmap(vbuf, len);
   close(testfile);
-  if (! result) {
+  if (EverParseIsError(result)) {
     printf(\"Witness from %s REJECTED\\n\", filename);
     return 1;
   };
@@ -1261,7 +1289,7 @@ let produce_test_checker_exe (out_file: string) (prog: prog) (name1: string) : M
   if None? args
   then failwith (Printf.sprintf "produce_test_checker_exe: parser %s not found" name1);
   let args = Some?.v args in
-  let modul, wrapper_name = module_and_wrapper_name name1 in
+  let modul, validator_name = module_and_validator_name name1 in
   with_out_file out_file (fun cout ->
-    cout (test_checker_c modul wrapper_name args)
+    cout (test_checker_c modul validator_name args)
   )