diff options
| author | Robert Norton | 2017-03-27 16:46:44 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-03-27 17:01:55 +0100 |
| commit | eb2fdf02e244873ef5d1ac74e37f7b00931e7c2d (patch) | |
| tree | 311cfcea928aeced3b910a64c0bdd3ae4c55443c /src | |
| parent | bc4633c84b0a3278c33d6d246a4d476683007a91 (diff) | |
Fix broken to_vec of negative values. Old code was a bit confused. Probably possible to rewrite using arithmetic on big_int which might be faster.
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_values.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index d6443a16..e8622a09 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -461,14 +461,14 @@ let rec divide_by_2_int array i n = then begin array.(i) <- Vone; divide_by_2_int array (i-1) quo end else divide_by_2_int array (i-1) quo -let rec add_one_bit array co i = +let rec add_one_bit array ci i = if i < 0 then array - else match array.(i),co with - | Vzero,false -> array.(i) <- Vone; array - | Vzero,true -> array.(i) <- Vone; add_one_bit array true (i-1) - | Vone, false -> array.(i) <- Vzero; add_one_bit array true (i-1) - | Vone, true -> add_one_bit array true (i-1) + else match array.(i),ci with + | Vzero,false -> add_one_bit array false (i-1) + | Vzero,true -> array.(i) <- Vone; add_one_bit array false (i-1) + | Vone, false -> array.(i) <- Vone; add_one_bit array false (i-1) + | Vone, true -> array.(i) <- Vzero; add_one_bit array true (i-1) | Vundef,_ -> assert false let to_vec_int ord len n = @@ -483,7 +483,7 @@ let to_vec_int ord len n = let abs_array = divide_by_2_int array (len-1) abs_n in let v_abs = bitwise_not (Vvector(abs_array,start,ord)) in match v_abs with - | Vvector(array,start,ord) -> Vvector(add_one_bit array false (len-1),start,ord) + | Vvector(array,start,ord) -> Vvector(add_one_bit array true (len-1),start,ord) | _ -> assert false let to_vec_big ord len n = @@ -499,7 +499,7 @@ let to_vec_big ord len n = let abs_array = divide_by_2_big array (len-1) abs_n in let v_abs = bitwise_not (Vvector(abs_array,start,ord)) in match v_abs with - | Vvector(array,start,ord) -> Vvector(add_one_bit array false (len-1),start,ord) + | Vvector(array,start,ord) -> Vvector(add_one_bit array true (len-1),start,ord) | _ -> assert false let to_vec_inc_int (len,n) = to_vec_int true len n |