Skip to content

Commit

Permalink
Fix two overzealous mono rewrites
Browse files Browse the repository at this point in the history
Quite hard to trip accidentally, especially as monomorphisation will
probably fail.
  • Loading branch information
bacam committed Aug 24, 2023
1 parent ae8e8bc commit 584641d
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/lib/monomorphise.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3308,12 +3308,13 @@ module MonoRewrites = struct
(* subrange == ones *)
| [E_aux (E_app (subrange1, [vector1; start1; end1]), _); E_aux (E_app (ones2, [_]), _)]
when is_id env (Id "vector_subrange") subrange1
&& is_ones ones2
&& is_bitvector_typ (typ_of vector1)
&& not (is_constant_range (start1, end1)) ->
E_app (mk_id "is_ones_subrange", [vector1; start1; end1])
(* slice == ones *)
| [E_aux (E_app (slice1, [vector1; start1; len1]), _); E_aux (E_app (ones2, [_]), _)]
when is_slice slice1 && (not (is_constant len1)) && is_bitvector_typ (typ_of vector1) ->
when is_slice slice1 && is_ones ones2 && (not (is_constant len1)) && is_bitvector_typ (typ_of vector1) ->
E_app (mk_id "is_ones_slice", [vector1; start1; len1])
(* Arm specs sometimes check for overflows on values that can be either 32 or 64 bits
by converting to unbounded integers and asking for the top slice. *)
Expand Down

0 comments on commit 584641d

Please sign in to comment.