diff --git a/src/3d/Z3TestGen.fst b/src/3d/Z3TestGen.fst index 1f6732054..b71360a43 100644 --- a/src/3d/Z3TestGen.fst +++ b/src/3d/Z3TestGen.fst @@ -864,13 +864,6 @@ let rec read_witness_args (z3: Z3.z3) (accu: list string) (n: nat) : ML (list st read_witness_args z3 (arg :: accu) n' end -let module_and_wrapper_name - (s: string) -: ML (string & string) -= match String.split ['.'] s with - | [modul; fn] -> modul, Target.wrapper_name modul fn - | _ -> failwith "Z3TestGen.wrapper_name" - let module_and_validator_name (s: string) : ML (string & string) @@ -895,23 +888,23 @@ let rec print_witness_args_as_c let print_witness_call_as_c_aux (out: (string -> ML unit)) - (wrapper_name: string) + (validator_name: string) (arg_types: list arg_type) (witness_length: nat) (args: list string) : ML unit = - out wrapper_name; + out validator_name; out "("; print_witness_args_as_c out arg_types args; - out "witness, "; + out "&context, &TestErrorHandler, witness, "; out (string_of_int witness_length); - out ");" + out ", 0);" let print_witness_call_as_c (out: (string -> ML unit)) (positive: bool) - (wrapper_name: string) + (validator_name: string) (arg_types: list arg_type) (witness_length: nat) (args: list string) @@ -919,13 +912,27 @@ let print_witness_call_as_c = out " { - BOOLEAN result = "; - print_witness_call_as_c_aux out wrapper_name arg_types witness_length args; + uint8_t context = 0; + uint64_t output = "; + print_witness_call_as_c_aux out validator_name arg_types witness_length args; out " printf(\" "; - print_witness_call_as_c_aux out wrapper_name arg_types witness_length args; + print_witness_call_as_c_aux out validator_name arg_types witness_length args; out " // \"); - if (result) printf (\"ACCEPTED\\n\\n\"); else printf (\"REJECTED\\n\\n\"); + BOOLEAN result = !EverParseIsError(output); + BOOLEAN consumes_all_bytes_if_successful = true; + if (result) { + consumes_all_bytes_if_successful = (output == "; + out (string_of_int witness_length); + out "U); + result = consumes_all_bytes_if_successful; + } + if (result) + printf (\"ACCEPTED\\n\\n\"); + else if (!consumes_all_bytes_if_successful) + printf (\"REJECTED (not all bytes consumed)\\n\\n\"); + else + printf (\"REJECTED (failed)\\n\\n\"); if ("; if positive then out "!"; out "result) @@ -970,26 +977,26 @@ let print_witness_as_c_gen let print_witness_as_c (out: (string -> ML unit)) (positive: bool) - (wrapper_name: string) + (validator_name: string) (arg_types: list arg_type) (witness: Seq.seq int) (args: list string) : ML unit = print_witness_as_c_gen out witness (fun len -> - print_witness_call_as_c out positive wrapper_name arg_types len args + print_witness_call_as_c out positive validator_name arg_types len args ) let print_diff_witness_as_c (out: (string -> ML unit)) - (wrapper_name1: string) - (wrapper_name2: string) + (validator_name1: string) + (validator_name2: string) (arg_types: list arg_type) (witness: Seq.seq int) (args: list string) : ML unit = print_witness_as_c_gen out witness (fun len -> - print_witness_call_as_c out true wrapper_name1 arg_types len args; - print_witness_call_as_c out false wrapper_name2 arg_types len args + print_witness_call_as_c out true validator_name1 arg_types len args; + print_witness_call_as_c out false validator_name2 arg_types len args ) let print_witness (witness: Seq.seq int) : ML unit = @@ -1074,7 +1081,7 @@ Printf.sprintf " let mk_get_first_positive_test_witness (name: string) (l: list arg_type) : string = mk_get_witness name l ^ " -(assert (>= state-witness-input-size 0)) +(assert (= (input-size state-witness) 0)) ; validator shall consume all input " let rec mk_choose_conj (witness: Seq.seq int) (accu: string) (i: nat) : Tot string @@ -1098,7 +1105,28 @@ let mk_want_another_distinct_witness witness witness_args : Tot string = let mk_get_first_negative_test_witness (name: string) (l: list arg_type) : string = mk_get_witness name l ^ " -(assert (< state-witness-input-size 0)) +(assert (< state-witness-input-size 0)) ; validator shall genuinely fail, we are not interested in positive cases followed by garbage +" + +let test_error_handler = " +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; + } +} " let do_test (out_file: option string) (z3: Z3.z3) (prog: prog) (name1: string) (nbwitnesses: int) (pos: bool) (neg: bool) : ML unit = @@ -1106,23 +1134,27 @@ let do_test (out_file: option string) (z3: Z3.z3) (prog: prog) (name1: string) ( if None? args then failwith (Printf.sprintf "do_test: 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 let nargs = count_args args in with_option_out_file out_file (fun cout -> cout "#include +#include #include \""; cout modul; - cout "Wrapper.h\" + cout ".h\" +"; + cout test_error_handler; + cout " int main(void) { "; if pos then begin FStar.IO.print_string (Printf.sprintf ";; Positive test witnesses for %s\n" name1); - witnesses_for (print_witness_as_c cout true wrapper_name args) z3 name1 args nargs (mk_get_first_positive_test_witness name1 args) mk_want_another_distinct_witness nbwitnesses + witnesses_for (print_witness_as_c cout true validator_name args) z3 name1 args nargs (mk_get_first_positive_test_witness name1 args) mk_want_another_distinct_witness nbwitnesses end; if neg then begin FStar.IO.print_string (Printf.sprintf ";; Negative test witnesses for %s\n" name1); - witnesses_for (print_witness_as_c cout false wrapper_name args) z3 name1 args nargs (mk_get_first_negative_test_witness name1 args) mk_want_another_distinct_witness nbwitnesses + witnesses_for (print_witness_as_c cout false validator_name args) z3 name1 args nargs (mk_get_first_negative_test_witness name1 args) mk_want_another_distinct_witness nbwitnesses end; cout " return 0; } @@ -1133,14 +1165,14 @@ let mk_get_first_diff_test_witness (name1: string) (l: list arg_type) (name2: st Printf.sprintf " %s -(assert (< (input-size (%s initial-state)) 0)) +(assert (not (= (input-size (%s initial-state)) 0))) ; test cases that do not consume everything are considered failing " (mk_get_first_positive_test_witness name1 l) (mk_call_args name2 0 l) -let do_diff_test_for (cout: string -> ML unit) (z3: Z3.z3) (prog: prog) name1 name2 args (nargs: nat { nargs == count_args args }) wrapper_name1 wrapper_name2 nbwitnesses = +let do_diff_test_for (cout: string -> ML unit) (z3: Z3.z3) (prog: prog) name1 name2 args (nargs: nat { nargs == count_args args }) validator_name1 validator_name2 nbwitnesses = FStar.IO.print_string (Printf.sprintf ";; Witnesses that work with %s but not with %s\n" name1 name2); - witnesses_for (print_diff_witness_as_c cout wrapper_name1 wrapper_name2 args) z3 name1 args nargs (mk_get_first_diff_test_witness name1 args name2) mk_want_another_distinct_witness nbwitnesses + witnesses_for (print_diff_witness_as_c cout validator_name1 validator_name2 args) z3 name1 args nargs (mk_get_first_diff_test_witness name1 args name2) mk_want_another_distinct_witness nbwitnesses let do_diff_test (out_file: option string) (z3: Z3.z3) (prog: prog) name1 name2 nbwitnesses = let args = List.assoc name1 prog in @@ -1153,26 +1185,29 @@ let do_diff_test (out_file: option string) (z3: Z3.z3) (prog: prog) name1 name2 if args2 <> Some args then failwith (Printf.sprintf "do_diff_test: parsers %s and %s do not have the same arg types" name1 name2); let nargs = count_args args in - let modul1, wrapper_name1 = module_and_wrapper_name name1 in - let modul2, wrapper_name2 = module_and_wrapper_name name2 in + let modul1, validator_name1 = module_and_validator_name name1 in + let modul2, validator_name2 = module_and_validator_name name2 in with_option_out_file out_file (fun cout -> cout "#include +#include #include \""; cout modul1; - cout "Wrapper.h\" + cout ".h\" #include \""; cout modul2; - cout "Wrapper.h\" + cout ".h\" +"; + cout test_error_handler; + cout " int main(void) { "; - do_diff_test_for cout z3 prog name1 name2 args nargs wrapper_name1 wrapper_name2 nbwitnesses; - do_diff_test_for cout z3 prog name2 name1 args nargs wrapper_name2 wrapper_name1 nbwitnesses; + do_diff_test_for cout z3 prog name1 name2 args nargs validator_name1 validator_name2 nbwitnesses; + do_diff_test_for cout z3 prog name2 name1 args nargs validator_name2 validator_name1 nbwitnesses; cout " return 0; } " ) - let test_exe_mk_arg (accu: (int & string & string & string)) (p: arg_type) @@ -1220,24 +1255,7 @@ let test_checker_c #include #include -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; - } -} +"^test_error_handler^" int main(int argc, char** argv) { if (argc < "^nb_cmd_and_args_s^") { diff --git a/src/3d/tests/TestSMT.3d b/src/3d/tests/TestSMT.3d index 81fb495d7..dbdb4bb39 100644 --- a/src/3d/tests/TestSMT.3d +++ b/src/3d/tests/TestSMT.3d @@ -9,3 +9,10 @@ typedef struct test2 { UINT8 x { x >= 10 }; UINT8 y { (UINT16)x + (UINT16)y <= 30 }; } test2_t; + +entrypoint +typedef struct test3 { + UINT8 x { x >= 10 }; + UINT8 y { (UINT16)x + (UINT16)y <= 30 }; + UINT8 rab; +} test3_t;