Skip to content

Commit

Permalink
Fix issue with vector bitcast.
Browse files Browse the repository at this point in the history
Ensure that types are evenly divisible so the vector is appropriately
sized.

All QC tests seem to be passing again.
  • Loading branch information
Chobbes committed Apr 3, 2024
1 parent d390c2a commit 0ec9b22
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/coq/QC/GenAST.v
Original file line number Diff line number Diff line change
Expand Up @@ -2675,7 +2675,8 @@ Section InstrGenerators.
let trivial_typs := [(* (1%N, TYPE_I 1); *) (8%N, TYPE_I 8); (32%N, TYPE_I 32); (32%N, TYPE_Float); (64%N, TYPE_I 64) (* ; (64%N, TYPE_Double) *)] in
let size_of_vec := get_bit_size_from_typ t_from in
let choices := fold_left (fun acc '(s,t) => let sz' := (size_of_vec / s)%N in
if (sz' =? 0)%N then acc else ((TYPE_Vector sz' t) :: acc)%list) trivial_typs [] in
let rem := (size_of_vec mod s)%N in
if ((sz' =? 0) || negb (rem =? 0))%N then acc else ((TYPE_Vector sz' t) :: acc)%list) trivial_typs [] in
ret (t_from :: choices) (* I think adding t_from here slightly biases the generator sometimes *)
end
| TYPE_Pointer subtyp =>
Expand Down

0 comments on commit 0ec9b22

Please sign in to comment.