Skip to content

Commit

Permalink
support for bitvector slicing
Browse files Browse the repository at this point in the history
  • Loading branch information
fvogels committed Nov 27, 2024
1 parent 7dd3181 commit f3e1185
Showing 1 changed file with 38 additions and 0 deletions.
38 changes: 38 additions & 0 deletions nanosail/NanosailToMicrosail/FunctionCalls.ml
Original file line number Diff line number Diff line change
Expand Up @@ -479,6 +479,40 @@ let translate_bitvector_concatenation (arguments : Ast.Expression.t list) : PP.d
| _ -> GC.fail @@ Printf.sprintf "%s should receive two bitvector arguments" sail_name


let translate_bitvector_slicing (arguments : Ast.Expression.t list) : PP.document GC.t =
let sail_name = "subrange_bits"
in
match arguments with
| [bitvector; first_index; second_index] -> begin
(*
How indices need to be interpreted depends on the order
Here we assume that "backward slices" are not possible, i.e.,
that the range goes from the lowest index to the highest index.
*)
let* pp_bitvector = Expressions.pp_expression bitvector
and* first_index = extract_compile_time_integer first_index
and* second_index = extract_compile_time_integer second_index
in
match first_index, second_index with
| Some first_index, Some second_index -> begin
let first_index = Z.to_int first_index
and second_index = Z.to_int second_index
in
let low_index = Int.min first_index second_index
and high_index = Int.max first_index second_index
in
let length = high_index - low_index + 1
in
translate_unary_operator
(Ast.Identifier.mk sail_name)
(Printf.sprintf "(uop.vector_subrange %d %d)" low_index length)
[ PP.(surround parens) pp_bitvector ]
end
| _ -> GC.fail @@ Printf.sprintf "%s's indices should be known at compile time" sail_name
end
| _ -> GC.fail @@ Printf.sprintf "%s should receive three arguments" sail_name


let translate
(function_identifier : Ast.Identifier.t )
(arguments : Ast.Expression.t list) : PP.document GC.t
Expand Down Expand Up @@ -608,6 +642,10 @@ let translate
GC.pp_annotate [%here] begin
translate_bitvector_concatenation arguments
end
| "subrange_bits" ->
GC.pp_annotate [%here] begin
translate_bitvector_slicing arguments
end
| _ ->
GC.pp_annotate [%here] begin
GC.return @@ MuSail.Statement.pp_call function_identifier pp_arguments
Expand Down

0 comments on commit f3e1185

Please sign in to comment.