rems-project / sail

Sail architecture definition language
Other
622 stars 116 forks source link

Lean: Translate bit vectors with constant width #755

Closed javra closed 3 weeks ago

javra commented 3 weeks ago

Sticking to the plan of not caring too much about superfluous parentheses because we'll remove them with a Lean based formatter.

Translates

default Order dec

$include <prelude.sail>

function extern_const() -> bitvector(64) = {
  return 0xFFFF_0000_1234_0000
}

function extern_add() -> bitvector(16) = {
  return 0xFFFF + 0x1234
}

to

def extern_const : BitVec 64 :=
  (0xFFFF000012340000 : BitVec 64)

def extern_add : BitVec 16 :=
  (Add.add (0xFFFF : BitVec 16) (0x1234 : BitVec 16))

def initialize_registers : Unit :=
  ()
github-actions[bot] commented 3 weeks ago

Test Results

   10 files  ±0     22 suites  ±0   0s ⏱️ ±0s   704 tests ±0    704 ✅ ±0  0 💤 ±0  0 ❌ ±0  2 196 runs  ±0  2 195 ✅ ±0  1 💤 ±0  0 ❌ ±0 

Results for commit 65856cf6. ± Comparison against base commit 9f8d0b7e.