Add flag for match bv

Author: ineol

src/sail_lean_backend/sail_plugin_lean.ml

@@ -81,6 +81,10 @@ let opt_lean_real_numbers : bool ref = ref false
 
 let opt_single_file : bool ref = ref false
 
+(* We keep two flags to use the [If_flag] in the list of rewrites. They should never be equal. *)
+let opt_enable_matchbv : bool ref = ref false
+let opt_disable_matchbv : bool ref = ref true
+
 let lean_version : string = "lean4:nightly-2025-04-07"
 let mathlib_version : string = "nightly-testing-2025-04-07"
 
@@ -98,6 +102,14 @@ let lean_options =
       Arg.Unit (fun () -> opt_single_file := true),
       "puts the entire output in a single .lean file"
     );
+    ( Flag.create ~prefix:["lean"] "matchbv",
+      Arg.Unit
+        (fun () ->
+          opt_disable_matchbv := false;
+          opt_enable_matchbv := true
+        ),
+      "use matchbv in the Lean output"
+    );
     ( Flag.create ~prefix:["lean"] "noncomputable",
       Arg.Unit (fun () -> opt_lean_noncomputable := true),
       "add a 'noncomputable section' at the beginning of the output"
@@ -141,11 +153,12 @@ let lean_rewrites =
     ("tuple_assignments", []);
     ("vector_concat_assignments", []);
     ("simple_assignments", []);
-    (* ("remove_vector_concat", []); *)
-    (* ("remove_bitvector_pats", []); *)
+    ("remove_vector_concat", [If_flag opt_disable_matchbv]);
+    ("remove_bitvector_pats", [If_flag opt_disable_matchbv]);
     (* ("remove_numeral_pats", []); *)
     (* ("pattern_literals", [Literal_arg "lem"]); *)
-    ("fun_guarded_pats", []);
+    ("fun_guarded_pats", [If_flag opt_enable_matchbv]);
+    ("guarded_pats", [If_flag opt_disable_matchbv]);
     (* ("register_ref_writes", rewrite_register_ref_writes); *)
     ("nexp_ids", []);
     ("split", [String_arg "execute"]);
@@ -164,7 +177,7 @@ let lean_rewrites =
     (* We need to do the exhaustiveness check before merging, because it may
        introduce new wildcard clauses *)
     ("recheck_defs", []);
-    (* ("make_cases_exhaustive", []); *)
+    ("make_cases_exhaustive", [If_flag opt_disable_matchbv]);
     (* merge funcls before adding the measure argument so that it doesn't
        disappear into an internal pattern match *)
     ("merge_function_clauses", []);

test/lean/SailTinyArm.expected.lean

@@ -508,7 +508,7 @@ open CacheOp
 open Barrier
 open AccessType
 
-/-- Type quantifiers: k_ex5891# : Bool, k_ex5890# : Bool -/
+/-- Type quantifiers: k_ex6347# : Bool, k_ex6346# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (Bool.not (BEq.beq x y))
 
@@ -1936,14 +1936,42 @@ def execute (merge_var : ast) : SailM Unit := do
   | .DataMemoryBarrier arg0 => (execute_DataMemoryBarrier arg0)
   | .CompareAndBranch (t, offset) => (execute_CompareAndBranch t offset)
 
-def decode (merge_var : (BitVec 32)) : (Option ast) :=
-  match_bv merge_var with
-  | [11,111,0,00,opc:2,1,Rm:5,option_v:3,S,10,Rn:5,Rt:5] =>
-    (decodeLoadStoreRegister opc Rm option_v S Rn Rt)
-  | [sf,10,01010,shift:2,N,Rm:5,imm6:6,Rn:5,Rd:5] => (decodeExclusiveOr sf shift N Rm imm6 Rn Rd)
-  | [1101010100,0,00,011,0011,CRm:4,1,01,11111] => (decodeDataMemoryBarrier CRm)
-  | [1,011010,0,imm19:19,Rt:5] => (decodeCompareAndBranch imm19 Rt)
-  | _ => none
+def decode (v__0 : (BitVec 32)) : (Option ast) :=
+  bif (Bool.and (BEq.beq (Sail.BitVec.extractLsb v__0 31 24) (0xF8 : (BitVec 8)))
+       (Bool.and (BEq.beq (Sail.BitVec.extractLsb v__0 21 21) (0b1 : (BitVec 1)))
+         (BEq.beq (Sail.BitVec.extractLsb v__0 11 10) (0b10 : (BitVec 2)))))
+  then
+    (let S := (BitVec.access v__0 12)
+    let option_v : (BitVec 3) := (Sail.BitVec.extractLsb v__0 15 13)
+    let opc : (BitVec 2) := (Sail.BitVec.extractLsb v__0 23 22)
+    let Rt : (BitVec 5) := (Sail.BitVec.extractLsb v__0 4 0)
+    let Rn : (BitVec 5) := (Sail.BitVec.extractLsb v__0 9 5)
+    let Rm : (BitVec 5) := (Sail.BitVec.extractLsb v__0 20 16)
+    (decodeLoadStoreRegister opc Rm option_v S Rn Rt))
+  else
+    (bif (BEq.beq (Sail.BitVec.extractLsb v__0 30 24) (0b1001010 : (BitVec 7)))
+    then
+      (let sf := (BitVec.access v__0 31)
+      let N := (BitVec.access v__0 21)
+      let shift : (BitVec 2) := (Sail.BitVec.extractLsb v__0 23 22)
+      let imm6 : (BitVec 6) := (Sail.BitVec.extractLsb v__0 15 10)
+      let Rn : (BitVec 5) := (Sail.BitVec.extractLsb v__0 9 5)
+      let Rm : (BitVec 5) := (Sail.BitVec.extractLsb v__0 20 16)
+      let Rd : (BitVec 5) := (Sail.BitVec.extractLsb v__0 4 0)
+      (decodeExclusiveOr sf shift N Rm imm6 Rn Rd))
+    else
+      (bif (Bool.and (BEq.beq (Sail.BitVec.extractLsb v__0 31 12) (0xD5033 : (BitVec 20)))
+           (BEq.beq (Sail.BitVec.extractLsb v__0 7 0) (0xBF : (BitVec 8))))
+      then
+        (let CRm : (BitVec 4) := (Sail.BitVec.extractLsb v__0 11 8)
+        (decodeDataMemoryBarrier CRm))
+      else
+        (bif (BEq.beq (Sail.BitVec.extractLsb v__0 31 24) (0xB4 : (BitVec 8)))
+        then
+          (let imm19 : (BitVec 19) := (Sail.BitVec.extractLsb v__0 23 5)
+          let Rt : (BitVec 5) := (Sail.BitVec.extractLsb v__0 4 0)
+          (decodeCompareAndBranch imm19 Rt))
+        else none)))
 
 def iFetch (addr : (BitVec 64)) : SailM (BitVec 32) := do
   let req : (Mem_read_request 4 64 (BitVec 56) (Option TranslationInfo) arm_acc_type) :=

test/lean/append.expected.lean

@@ -45,7 +45,7 @@ namespace Out.Functions
 
 open option
 
-/-- Type quantifiers: k_ex688# : Bool, k_ex687# : Bool -/
+/-- Type quantifiers: k_ex699# : Bool, k_ex698# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (Bool.not (BEq.beq x y))
 

test/lean/bitfield.expected.lean

@@ -55,7 +55,7 @@ namespace Out.Functions
 open option
 open Register
 
-/-- Type quantifiers: k_ex689# : Bool, k_ex688# : Bool -/
+/-- Type quantifiers: k_ex700# : Bool, k_ex699# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (Bool.not (BEq.beq x y))
 

test/lean/bitvec_operation.expected.lean

@@ -45,7 +45,7 @@ namespace Out.Functions
 
 open option
 
-/-- Type quantifiers: k_ex807# : Bool, k_ex806# : Bool -/
+/-- Type quantifiers: k_ex820# : Bool, k_ex819# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (Bool.not (BEq.beq x y))
 

test/lean/early_return.expected.lean

@@ -65,7 +65,7 @@ open option
 open Register
 open E
 
-/-- Type quantifiers: k_ex2312# : Bool, k_ex2311# : Bool -/
+/-- Type quantifiers: k_ex2343# : Bool, k_ex2342# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (Bool.not (BEq.beq x y))
 
@@ -418,7 +418,7 @@ def match_early_return_loop (x : E) : SailM E := SailME.run do
   | C => writeReg r_C A
   readReg r_B
 
-/-- Type quantifiers: k_ex2624# : Bool -/
+/-- Type quantifiers: k_ex2655# : Bool -/
 def ite_early_return (x : Bool) : SailM E := SailME.run do
   writeReg r_A (← readReg r_C)
   let y ← (( do
@@ -429,7 +429,7 @@ def ite_early_return (x : Bool) : SailM E := SailME.run do
     else readReg r_B ) : SailME _ E )
   readReg r_B
 
-/-- Type quantifiers: k_ex2626# : Bool -/
+/-- Type quantifiers: k_ex2657# : Bool -/
 def ite_early_return_inloop (x : Bool) : SailM E := SailME.run do
   let loop_i_lower := 0
   let loop_i_upper := 10
@@ -448,7 +448,7 @@ def ite_early_return_inloop (x : Bool) : SailM E := SailME.run do
   (pure loop_vars)
   readReg r_B
 
-/-- Type quantifiers: k_ex2630# : Bool -/
+/-- Type quantifiers: k_ex2661# : Bool -/
 def ite_early_return_loop (x : Bool) : SailM E := SailME.run do
   bif x
   then
@@ -468,7 +468,7 @@ def ite_early_return_loop (x : Bool) : SailM E := SailME.run do
 def unit_type (x : E) : SailM Unit := do
   writeReg r_A x
 
-/-- Type quantifiers: k_ex2634# : Bool -/
+/-- Type quantifiers: k_ex2665# : Bool -/
 def ite_early_return_seq (x : Bool) : SailM E := SailME.run do
   writeReg r_A (← readReg r_C)
   let y ← (( do

test/lean/enum.expected.lean

@@ -49,7 +49,7 @@ namespace Out.Functions
 open option
 open E
 
-/-- Type quantifiers: k_ex706# : Bool, k_ex705# : Bool -/
+/-- Type quantifiers: k_ex717# : Bool, k_ex716# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (Bool.not (BEq.beq x y))
 

test/lean/errors.expected.lean

@@ -53,7 +53,7 @@ namespace Out.Functions
 open option
 open Register
 
-/-- Type quantifiers: k_ex716# : Bool, k_ex715# : Bool -/
+/-- Type quantifiers: k_ex731# : Bool, k_ex730# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (Bool.not (BEq.beq x y))
 
@@ -124,13 +124,13 @@ def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
 def concat_str_dec (str : String) (x : Int) : String :=
   (HAppend.hAppend str (Int.repr x))
 
-/-- Type quantifiers: k_ex809# : Bool -/
+/-- Type quantifiers: k_ex824# : Bool -/
 def test_exit (b : Bool) : SailM Unit := do
   bif b
   then throw Error.Exit
   else (pure ())
 
-/-- Type quantifiers: k_ex811# : Bool -/
+/-- Type quantifiers: k_ex826# : Bool -/
 def test_assert (b : Bool) : SailM (BitVec 1) := do
   assert b "b is false"
   (pure 1#1)

test/lean/extern.expected.lean

@@ -45,7 +45,7 @@ namespace Out.Functions
 
 open option
 
-/-- Type quantifiers: k_ex1150# : Bool, k_ex1149# : Bool -/
+/-- Type quantifiers: k_ex1162# : Bool, k_ex1161# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (Bool.not (BEq.beq x y))
 
@@ -166,12 +166,10 @@ def sep_backwards (arg_ : String) : SailM Unit := do
 def sep_forwards_matches (arg_ : Unit) : Bool :=
   match arg_ with
   | () => true
-  | _ => false
 
 def sep_backwards_matches (arg_ : String) : SailM Bool := do
   match arg_ with
   | _ => throw Error.Exit
-  | _ => (pure false)
 
 def extern_add (_ : Unit) : Int :=
   (5 +i 4)

test/lean/extern_bitvec.expected.lean

@@ -45,7 +45,7 @@ namespace Out.Functions
 
 open option
 
-/-- Type quantifiers: k_ex718# : Bool, k_ex717# : Bool -/
+/-- Type quantifiers: k_ex729# : Bool, k_ex728# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (Bool.not (BEq.beq x y))