Add lsl and lsr support.
This commit is contained in:
parent
8232eecc6e
commit
9433fa9bc4
@ -20,7 +20,7 @@ let is_pure_constant : constant -> bool =
|
|||||||
| C_UNIT
|
| C_UNIT
|
||||||
| C_CAR | C_CDR | C_PAIR
|
| C_CAR | C_CDR | C_PAIR
|
||||||
| C_NIL | C_CONS
|
| C_NIL | C_CONS
|
||||||
| C_NEG | C_OR | C_AND | C_XOR | C_NOT
|
| C_NEG | C_OR | C_AND | C_LSL | C_LSR | C_XOR | C_NOT
|
||||||
| C_EQ | C_NEQ | C_LT | C_LE | C_GT | C_GE
|
| C_EQ | C_NEQ | C_LT | C_LE | C_GT | C_GE
|
||||||
| C_SOME
|
| C_SOME
|
||||||
| C_UPDATE | C_MAP_GET | C_MAP_FIND_OPT | C_MAP_ADD | C_MAP_UPDATE
|
| C_UPDATE | C_MAP_GET | C_MAP_FIND_OPT | C_MAP_ADD | C_MAP_UPDATE
|
||||||
|
@ -87,6 +87,8 @@ module Simplify = struct
|
|||||||
| "bitwise_or" -> ok C_OR
|
| "bitwise_or" -> ok C_OR
|
||||||
| "bitwise_and" -> ok C_AND
|
| "bitwise_and" -> ok C_AND
|
||||||
| "bitwise_xor" -> ok C_XOR
|
| "bitwise_xor" -> ok C_XOR
|
||||||
|
| "bitwise_lsl" -> ok C_LSL
|
||||||
|
| "bitwise_lsr" -> ok C_LSR
|
||||||
| "string_concat" -> ok C_CONCAT
|
| "string_concat" -> ok C_CONCAT
|
||||||
| "string_slice" -> ok C_SLICE
|
| "string_slice" -> ok C_SLICE
|
||||||
| "crypto_check" -> ok C_CHECK_SIGNATURE
|
| "crypto_check" -> ok C_CHECK_SIGNATURE
|
||||||
@ -210,6 +212,8 @@ module Simplify = struct
|
|||||||
| "Bitwise.lor" -> ok C_OR
|
| "Bitwise.lor" -> ok C_OR
|
||||||
| "Bitwise.land" -> ok C_AND
|
| "Bitwise.land" -> ok C_AND
|
||||||
| "Bitwise.lxor" -> ok C_XOR
|
| "Bitwise.lxor" -> ok C_XOR
|
||||||
|
| "Bitwise.shift_left" -> ok C_LSL
|
||||||
|
| "Bitwise.shift_right" -> ok C_LSR
|
||||||
|
|
||||||
| "String.length" -> ok C_SIZE
|
| "String.length" -> ok C_SIZE
|
||||||
| "String.size" -> ok C_SIZE
|
| "String.size" -> ok C_SIZE
|
||||||
@ -396,6 +400,8 @@ module Typer = struct
|
|||||||
| C_AND -> ok @@ failwith "t_and" ;
|
| C_AND -> ok @@ failwith "t_and" ;
|
||||||
| C_OR -> ok @@ failwith "t_or" ;
|
| C_OR -> ok @@ failwith "t_or" ;
|
||||||
| C_XOR -> ok @@ failwith "t_xor" ;
|
| C_XOR -> ok @@ failwith "t_xor" ;
|
||||||
|
| C_LSL -> ok @@ failwith "t_lsl" ;
|
||||||
|
| C_LSR -> ok @@ failwith "t_lsr" ;
|
||||||
(* COMPARATOR *)
|
(* COMPARATOR *)
|
||||||
| C_EQ -> ok @@ failwith "t_comparator EQ" ;
|
| C_EQ -> ok @@ failwith "t_comparator EQ" ;
|
||||||
| C_NEQ -> ok @@ failwith "t_comparator NEQ" ;
|
| C_NEQ -> ok @@ failwith "t_comparator NEQ" ;
|
||||||
@ -1006,6 +1012,8 @@ module Typer = struct
|
|||||||
| C_AND -> ok @@ and_ ;
|
| C_AND -> ok @@ and_ ;
|
||||||
| C_OR -> ok @@ or_ ;
|
| C_OR -> ok @@ or_ ;
|
||||||
| C_XOR -> ok @@ xor ;
|
| C_XOR -> ok @@ xor ;
|
||||||
|
| C_LSL -> ok @@ lsl_;
|
||||||
|
| C_LSR -> ok @@ lsr_;
|
||||||
(* COMPARATOR *)
|
(* COMPARATOR *)
|
||||||
| C_EQ -> ok @@ comparator "EQ" ;
|
| C_EQ -> ok @@ comparator "EQ" ;
|
||||||
| C_NEQ -> ok @@ comparator "NEQ" ;
|
| C_NEQ -> ok @@ comparator "NEQ" ;
|
||||||
@ -1103,6 +1111,8 @@ module Compiler = struct
|
|||||||
| C_OR -> ok @@ simple_binary @@ prim I_OR
|
| C_OR -> ok @@ simple_binary @@ prim I_OR
|
||||||
| C_AND -> ok @@ simple_binary @@ prim I_AND
|
| C_AND -> ok @@ simple_binary @@ prim I_AND
|
||||||
| C_XOR -> ok @@ simple_binary @@ prim I_XOR
|
| C_XOR -> ok @@ simple_binary @@ prim I_XOR
|
||||||
|
| C_LSL -> ok @@ simple_binary @@ prim I_LSL
|
||||||
|
| C_LSR -> ok @@ simple_binary @@ prim I_LSR
|
||||||
| C_NOT -> ok @@ simple_unary @@ prim I_NOT
|
| C_NOT -> ok @@ simple_unary @@ prim I_NOT
|
||||||
| C_PAIR -> ok @@ simple_binary @@ prim I_PAIR
|
| C_PAIR -> ok @@ simple_binary @@ prim I_PAIR
|
||||||
| C_CAR -> ok @@ simple_unary @@ prim I_CAR
|
| C_CAR -> ok @@ simple_unary @@ prim I_CAR
|
||||||
|
@ -45,6 +45,8 @@ let constant ppf : constant -> unit = function
|
|||||||
| C_AND -> fprintf ppf "AND"
|
| C_AND -> fprintf ppf "AND"
|
||||||
| C_OR -> fprintf ppf "OR"
|
| C_OR -> fprintf ppf "OR"
|
||||||
| C_XOR -> fprintf ppf "XOR"
|
| C_XOR -> fprintf ppf "XOR"
|
||||||
|
| C_LSL -> fprintf ppf "LSL"
|
||||||
|
| C_LSR -> fprintf ppf "LSR"
|
||||||
(* COMPARATOR *)
|
(* COMPARATOR *)
|
||||||
| C_EQ -> fprintf ppf "EQ"
|
| C_EQ -> fprintf ppf "EQ"
|
||||||
| C_NEQ -> fprintf ppf "NEQ"
|
| C_NEQ -> fprintf ppf "NEQ"
|
||||||
|
@ -162,6 +162,8 @@ type constant =
|
|||||||
| C_AND
|
| C_AND
|
||||||
| C_OR
|
| C_OR
|
||||||
| C_XOR
|
| C_XOR
|
||||||
|
| C_LSL
|
||||||
|
| C_LSR
|
||||||
(* COMPARATOR *)
|
(* COMPARATOR *)
|
||||||
| C_EQ
|
| C_EQ
|
||||||
| C_NEQ
|
| C_NEQ
|
||||||
|
@ -8,3 +8,9 @@ function and_op (const n : nat) : nat is
|
|||||||
|
|
||||||
function xor_op (const n : nat) : nat is
|
function xor_op (const n : nat) : nat is
|
||||||
begin skip end with bitwise_xor(n , 7n)
|
begin skip end with bitwise_xor(n , 7n)
|
||||||
|
|
||||||
|
function lsl_op (const n : nat) : nat is
|
||||||
|
begin skip end with bitwise_lsl(n , 7n)
|
||||||
|
|
||||||
|
function lsr_op (const n : nat) : nat is
|
||||||
|
begin skip end with bitwise_lsr(n , 7n)
|
@ -3,3 +3,5 @@
|
|||||||
let or_op (n: nat) : nat = Bitwise.lor n 4n
|
let or_op (n: nat) : nat = Bitwise.lor n 4n
|
||||||
let and_op (n: nat) : nat = Bitwise.land n 7n
|
let and_op (n: nat) : nat = Bitwise.land n 7n
|
||||||
let xor_op (n: nat) : nat = Bitwise.lxor n 7n
|
let xor_op (n: nat) : nat = Bitwise.lxor n 7n
|
||||||
|
let lsl_op (n: nat) : nat = Bitwise.shift_left n 7n
|
||||||
|
let lsr_op (n: nat) : nat = Bitwise.shift_right n 7n
|
||||||
|
@ -3,3 +3,5 @@
|
|||||||
let or_op = (n: nat): nat => Bitwise.lor(n, 4n);
|
let or_op = (n: nat): nat => Bitwise.lor(n, 4n);
|
||||||
let and_op = (n: nat): nat => Bitwise.land(n, 7n);
|
let and_op = (n: nat): nat => Bitwise.land(n, 7n);
|
||||||
let xor_op = (n: nat): nat => Bitwise.lxor(n, 7n);
|
let xor_op = (n: nat): nat => Bitwise.lxor(n, 7n);
|
||||||
|
let lsl_op = (n: nat) : nat => Bitwise.shift_left(n, 7n);
|
||||||
|
let lsr_op = (n: nat) : nat => Bitwise.shift_right(n, 7n);
|
@ -348,6 +348,8 @@ let bitwise_arithmetic () : unit result =
|
|||||||
let%bind () = expect_eq program "and_op" (e_nat 10) (e_nat 2) in
|
let%bind () = expect_eq program "and_op" (e_nat 10) (e_nat 2) in
|
||||||
let%bind () = expect_eq program "xor_op" (e_nat 0) (e_nat 7) in
|
let%bind () = expect_eq program "xor_op" (e_nat 0) (e_nat 7) in
|
||||||
let%bind () = expect_eq program "xor_op" (e_nat 7) (e_nat 0) in
|
let%bind () = expect_eq program "xor_op" (e_nat 7) (e_nat 0) in
|
||||||
|
let%bind () = expect_eq program "lsl_op" (e_nat 1000) (e_nat 128000) in
|
||||||
|
let%bind () = expect_eq program "lsr_op" (e_nat 128000) (e_nat 1000) in
|
||||||
ok ()
|
ok ()
|
||||||
|
|
||||||
let bitwise_arithmetic_mligo () : unit result =
|
let bitwise_arithmetic_mligo () : unit result =
|
||||||
@ -364,6 +366,8 @@ let bitwise_arithmetic_mligo () : unit result =
|
|||||||
let%bind () = expect_eq program "and_op" (e_nat 10) (e_nat 2) in
|
let%bind () = expect_eq program "and_op" (e_nat 10) (e_nat 2) in
|
||||||
let%bind () = expect_eq program "xor_op" (e_nat 0) (e_nat 7) in
|
let%bind () = expect_eq program "xor_op" (e_nat 0) (e_nat 7) in
|
||||||
let%bind () = expect_eq program "xor_op" (e_nat 7) (e_nat 0) in
|
let%bind () = expect_eq program "xor_op" (e_nat 7) (e_nat 0) in
|
||||||
|
let%bind () = expect_eq program "lsl_op" (e_nat 1000) (e_nat 128000) in
|
||||||
|
let%bind () = expect_eq program "lsr_op" (e_nat 128000) (e_nat 1000) in
|
||||||
ok ()
|
ok ()
|
||||||
|
|
||||||
let bitwise_arithmetic_religo () : unit result =
|
let bitwise_arithmetic_religo () : unit result =
|
||||||
@ -380,6 +384,8 @@ let bitwise_arithmetic_religo () : unit result =
|
|||||||
let%bind () = expect_eq program "and_op" (e_nat 10) (e_nat 2) in
|
let%bind () = expect_eq program "and_op" (e_nat 10) (e_nat 2) in
|
||||||
let%bind () = expect_eq program "xor_op" (e_nat 0) (e_nat 7) in
|
let%bind () = expect_eq program "xor_op" (e_nat 0) (e_nat 7) in
|
||||||
let%bind () = expect_eq program "xor_op" (e_nat 7) (e_nat 0) in
|
let%bind () = expect_eq program "xor_op" (e_nat 7) (e_nat 0) in
|
||||||
|
let%bind () = expect_eq program "lsl_op" (e_nat 1000) (e_nat 128000) in
|
||||||
|
let%bind () = expect_eq program "lsr_op" (e_nat 128000) (e_nat 1000) in
|
||||||
ok ()
|
ok ()
|
||||||
|
|
||||||
let string_arithmetic () : unit result =
|
let string_arithmetic () : unit result =
|
||||||
|
Loading…
Reference in New Issue
Block a user