Conversation
s-prism
force-pushed
the
x86-print-final-states
branch
from
be15e47 to
a7e0546
Compare
s-prism
changed the title
tperami
left a comment
tperami
left a comment
There was a problem hiding this comment.
Sorry I forgot to click "Submit review"
|
Also waiting on #102 |
s-prism
force-pushed
the
x86-print-final-states
branch
from
a7e0546 to
fd886c0
Compare
s-prism
force-pushed
the
x86-print-final-states
branch
from
309e179 to
1e12b40
Compare
| (conds : (Testrepr.thread_cond list * Testrepr.mem_cond list) list) : | ||
| (int * string) list * Testrepr.mem_cond list | ||
| = | ||
| (* Assuming that each (Testrepr.thread_cond list * Testrepr.mem_cond list) already contains unique values *) |
There was a problem hiding this comment.
That might not be the case, but on the other hand that's irrelevant to the code below
| (fun (acc_reg_cond, acc_mem_cond) (reg_cond, mem_cond) -> | ||
| let new_reg_cond = get_thread_regname_pairs reg_cond in | ||
| ( List.sort_uniq compare (acc_reg_cond @ new_reg_cond), | ||
| List.sort_uniq compare_mem_id (acc_mem_cond @ mem_cond) |
There was a problem hiding this comment.
This is resorting the list for every thread. Why don't you collect all and then run the sort at the end?
| in | ||
| assert_equal Runner.Expected result | ||
| ); | ||
| ("EOR Expected with seq model" |
There was a problem hiding this comment.
Those tests are getting removed in another PR, so please remove them, sorry
| @@ -0,0 +1,108 @@ | |||
| type reg_state = | |||
There was a problem hiding this comment.
This module needs top-level documentation and a copyright header (Please run make headers for that)
In particular, it needs to mention this if for mcompare-compatible output
| ) | ||
| states | ||
|
|
||
| let compare_minimised_states |
There was a problem hiding this comment.
I had no idea what this function did until I spend 5 min reading it, it needs a detailed comment
| (List.length state_list - obs_count) | ||
| test_name | ||
|
|
||
| let run_executions print_final_states model init fuel term test = |
There was a problem hiding this comment.
Can you make print_final_states a label argument? Raw boolean are hard to maintain.
| let run_executions print_final_states model init fuel term test = | |
| let run_executions ~print_final_states model init fuel term test = |
| - List.length | ||
| (List.fold_left | ||
| (fun unmatched_state_list (cond, mem_cond) -> | ||
| List.filter | ||
| (fun fs -> | ||
| not (check_outcome fs cond && check_mem_outcome fs mem_cond) | ||
| ) | ||
| unmatched_state_list | ||
| ) | ||
| state_list conds | ||
| ) |
There was a problem hiding this comment.
You should not have to recompute this
| ) | ||
| reg_cond | ||
|
|
||
| let compare_mem_id |
There was a problem hiding this comment.
| let compare_mem_id | |
| let compare_mem_sym |
| let conds = observable @ unobservable in | ||
| let unique_cond = MinimiseState.get_unique_conds_ignoring_value conds in | ||
| let minimised_fs = MinimiseState.minimise_states unique_cond final_states in | ||
| let unique_minimised_fs = | ||
| List.sort_uniq MinimiseState.compare_minimised_states minimised_fs | ||
| in |
There was a problem hiding this comment.
This should be a function in minState.ml
| ) | ||
| else msg "ERROR: no conditions to observe" | ||
| ) | ||
| ); |
There was a problem hiding this comment.
Most of this code should move to a separate function
3 participants
Test MP Allowed
States 3
1:rax=0; 1:rbx=0;
1:rax=0; 1:rbx=1;
1:rax=1; 1:rbx=1;
No (allowed not found)
Observation MP Never 0 3