Skip to content

Commit

Permalink
also reject z3 tests that are not fully consumed
Browse files Browse the repository at this point in the history
  • Loading branch information
@tahina-pro
tahina-pro committed Nov 1, 2023
1 parent 42d3192 commit 5adcc44
Show file tree
Hide file tree
Showing 2 changed files with 81 additions and 56 deletions.
130 changes: 74 additions & 56 deletions src/3d/Z3TestGen.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -895,37 +888,51 @@ 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)
: ML unit
=
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)
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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
Expand All @@ -1098,31 +1105,56 @@ 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 =
let args = List.assoc name1 prog in
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 <stdio.h>
#include <stdbool.h>
#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;
}
Expand All @@ -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
Expand All @@ -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 <stdio.h>
#include <stdbool.h>
#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)
Expand Down Expand Up @@ -1220,24 +1255,7 @@ let test_checker_c
#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;
}
}
"^test_error_handler^"
int main(int argc, char** argv) {
if (argc < "^nb_cmd_and_args_s^") {
Expand Down
7 changes: 7 additions & 0 deletions src/3d/tests/TestSMT.3d
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

0 comments on commit 5adcc44

Please sign in to comment.