module Sparc is 
  import [RTL Vector]
  from StdOperators import
    [add and andalso bit bitInsert bool borrow carry com divu
     modu muls mulu ne not or orelse quot shl shrl shra subtract sx xor zx
     --> := | ; = <> + - < <= > >= ? IEEE754
    ]
  from StdOperators.IEEE754 import
    [fadd fcmp fdiv f2f f2i fabs fmulx fsqrt i2f fmul fneg fsub]

  storage
    'm' is    cells of  8 bits called "memory" aggregate using RTL.AGGB
  storage
    'r' is 32 cells of 32 bits called "registers"
                fetch using \n. $r[n]
                store using \(n, v). n <> 0 --> RTL.TRUE_STORE ($r[n], v)
                aggregate using RTL.AGGB
  storage 'i' is 6 cells of 32 bits called "Integer-unit control/status registers"
  locations
    [PSR WIM TBR Y PC nPC] is $i[[0..5]]
    [EC EF S PS ET] is PSR@loc[1 bit at [13 12 7 6 5]]
  locations ICC is PSR@loc[20..23]
  rtlop carryBit : #4 bits -> #1 bits
  val carryBit is carryBit ICC
  fun byte  x  is  x :   #8 bits
  fun hword x  is  x :  #16 bits
  fun word  x  is  x :  #32 bits
  fun dword x  is  x :  #64 bits
  fun qword x  is  x : #128 bits
  locations
    [ g0  g1  g2  g3  g4  g5  g6  g7
      o0  o1  o2  o3  o4  o5  o6  o7
      l0  l1  l2  l3  l4  l5  l6  l7
      i0  i1  i2  i3  i4  i5  i6  i7 ] is $r[[0..31]]
    [sp fp] is [o6 i6]
  storage
    'f' is 32 cells of 32 bits called "floating-point registers"
           aggregate using RTL.AGGB
    'F' is  1 cell  of 32 bits called "floating-point state register (FSR)"
  locations
    FSR  is $F[0]
    RD   is FSR@loc[30..31]  --- rounding modes
    fcc  is FSR@loc[10..11]
  storage
    'c' is  cells of 32 bits called "coprocessor registers (implementation-dependent)"
                             aggregate using RTL.AGGB
    'C' is 1 cell of 32 bits called "coprocessor status register"  
  locations
    CSR is $C[0]
  storage 'b' is 1 cell of 1 bit called "store-barrier-pending flag"
  locations store_barrier_pending is $b[0]
  module Reg is 
    fun in'    n is $r[n+24]
    fun local' n is $r[n+16]
    fun out    n is $r[n+8]
    fun global n is $r[n]
  end
  storage
    'w' is    cells of 32 bits called "register windows"
    'W' is  1 cell  of 32 bits called "register-window pointer"
  locations
    winptr is $W[0]
    operand [ cd fd fs1 fs2 rd rdi rs1 rs1i rs2] : #5 bits
    operand asi : #8 bits
    operand simm13 : #13 bits
    operand imm22 : #22 bits
    operand target : #32 bits
    operand annul : #1 bits
  operand address : #32 bits
  default attribute of
    indexA(rs1, rs2)     is  $r[rs1] + $r[rs2]
    dispA (rs1, simm13)  is  $r[rs1] + sx simm13
  operand reg_or_imm : #32 bits
  default attribute of
    rmode (rs2)     is  $r[rs2]
    imode (simm13)  is  sx simm13
  storage 't' is 1 cell of 7 bits called "trap code" 
  locations trap_code is $t[0]
  fun trap k is $t[0] := k
  rtlop [data_store_error 
         illegal_instruction
         mem_address_not_aligned
         tag_overflow
        ] : #7 bits
  rtlop trap_instruction : #7 bits -> #7 bits
  fun alignTrap (address, k)  is  address modu k <> 0 --> trap(mem_address_not_aligned)
  fun saveOut   n is Reg.in' n         := Reg.out n
  fun saveLocal n is $w[winptr+8+zx n] := Reg.local' n
  fun saveIn    n is $w[winptr  +zx n] := Reg.in' n
  fun do8 f is Vector.foldr (\(n, effects). f n  | effects) RTL.SKIP (Vector.spanning 0 7)
  fun saveRegs rd is
    let fun saveOut   n is rd <> n+24 --> Reg.in' n := Reg.out n
        fun saveLocal n is $w[winptr+8+zx n] := Reg.local' n
        fun saveIn    n is $w[winptr+  zx n] := Reg.in' n
    in  do8 saveOut | do8 saveLocal | do8 saveIn | winptr := winptr + 16
    end
  fun restoreRegs rd is
    let fun restoreOut   n is rd <> n+8  --> Reg.out    n := Reg.in' n
        fun restoreLocal n is rd <> n+16 --> Reg.local' n := $w[winptr-8 +zx n]
        fun restoreIn    n is rd <> n+24 --> Reg.in'    n := $w[winptr-16+zx n]
    in  do8 restoreOut | do8 restoreLocal | do8 restoreIn | winptr := winptr - 16
    end
  fun [andn orn xnor] (a, b)  is  [and or xor](a, com b)
  rtlop encapsulate_cc : #32 bits * #1 bits * #1 bits -> #4 bits
  fun set_cc arg is ICC := encapsulate_cc arg
  fun leave_cc _ is RTL.SKIP
  fun logical_cc (result) is set_cc(result, 0, 0)
  fun binary (operator, rs1, r_o_i, rd) is $r[rd] := operator($r[rs1], r_o_i)
  fun binary_with_cc (operator, rs1, r_o_i, rd, special_cc) is 
    let val result is operator($r[rs1], r_o_i)
    in  $r[rd] := result | special_cc result
    end
  rtlop add_overflows : #n bits * #n bits * #1 bits -> bool
  fun add_instruction (rs1, operand2, carry_in, rd, {set_codes}) is 
    let val {result, carry is carry_out} is add($r[rs1], operand2, carry_in)
    in    $r[rd] := result
        | set_codes -->
            set_cc(result, bit(add_overflows ($r[rs1], operand2, carry_in)), carry_out)
    end
  module Reg64 is 
    fun set (reg, n) is Y := n@bits[32 bits at 32] | $r[reg] := n@bits[32 bits at 0]
    fun get reg      is bitInsert {wide is zx #32 #64 $r[reg], lsb is 32} Y
    fun get' reg     is bitInsert {wide is zx $r[reg], lsb is 32} Y : #64 bits
  end
  fun multiply (mul, rs1, r_o_i, rd, {set_codes}) is 
    let val result is mul($r[rs1], r_o_i)
    in  Reg64.set(rd, result) | set_codes --> set_cc (result, ?, ?)
    end
  fun mul_cc(result) is set_cc(result, ?, ?)
  module IccTest is 
    rtlop [A N NE E G LE GE L GU LEU CC CS POS NEG VC VS] : #4 bits -> bool
    val [A N NE E G LE GE L GU LEU CC CS POS NEG VC VS] is 
        [A N NE E G LE GE L GU LEU CC CS POS NEG VC VS] ICC : bool
    val tests is {A is A, N is N, NE is NE, E is E, G is G, LE is LE, GE is GE,
                  L is L, GU is GU, LEU is LEU, CC is CC, CS is CS, POS is POS,
                  NEG is NEG, VC is VC, VS is VS}
  end
  rtlop tag_overflows : #32 bits * #32 bits -> bool
  rtlop sub_overflows : #32 bits * #32 bits * #1 bits -> bool
  fun subtract_instruction (rs1, operand2, borrow, rd, {set_codes}) is 
    let val {result, borrow is borrow'} is subtract($r[rs1], operand2, borrow)
    in  $r[rd] := result
        | set_codes -->
            set_cc(result, bit(sub_overflows($r[rs1], operand2, borrow)), borrow')
    end
  rtlop [sparc_udiv_overflow sparc_sdiv_overflow] : #64 bits * #32 bits -> #1 bits
  fun divide({signed}, rs1, r_o_i, rd, {set_codes}) is
    let val (operator, overflow) is if signed then ((divu), sparc_udiv_overflow)
                                    else           ((quot), sparc_sdiv_overflow)
                                    fi
        val result is operator(Reg64.get rs1, r_o_i)
        val V      is overflow(Reg64.get rs1, r_o_i)
    in  $r[rd] := result | set_codes --> set_cc (result, V, 0)
    end
  default attribute of
    default attribute of
      ld^[s u]^[b h] (address, rd)  is  $r[rd] := [sx zx] ([byte word] $m[address])
    ld^["" d] (address, rd)  is $r[rd] := [word dword] $m[address] 
    sth       (rd, address)  is  $m[address] := $r[rd]@bits[16 bits at 0]
    stb       (rd, address)  is  $m[address] := $r[rd]@bits[ 8 bits at 0]
    st^["" d] (rd, address)  is  $m[address] := [word dword] $r[rd]
    ldstub(address, rd) is $r[rd] := zx $m[address] | $m[address] := 0xff
    swap  (address, rd) is $r[rd] :=    $m[address] | $m[address] := $r[rd]
    save (rs1, reg_or_imm, rd) is saveRegs rd | $r[rd] := $r[rs1] + reg_or_imm
    restore (rs1, reg_or_imm, rd) is restoreRegs rd | $r[rd] := $r[rs1] + reg_or_imm
    [and or xor andn orn xnor]^[cc ""] (rs1, reg_or_imm, rd) is
      binary_with_cc([and or xor andn orn xnor], rs1, reg_or_imm, rd, [logical_cc leave_cc])
    [add addcc addx addxcc] (rs1, reg_or_imm, rd) is 
       add_instruction(rs1, reg_or_imm, [0 carryBit], rd, {set_codes is [false true]})
    [u s]^mul^["" cc] (rs1, reg_or_imm, rd) is 
      multiply([mulu muls], rs1, reg_or_imm, rd, {set_codes is [false true]})
    b^[a n ne e g le ge l gu leu cc cs pos neg vc vs] (target, annul) is
      let val t is IccTest.tests
      in  [t.A  t.N   t.NE t.E  t.G   t.LE  t.GE t.L
           t.GU t.LEU t.CC t.CS t.POS t.NEG t.VC t.VS
          ]  --> nPC := target
      end
    call (target)      is nPC := target  | Reg.out 7 := PC
    jmpl (address, rd) is nPC := address | $r[rd]    := PC
    ld^[f df] (address, fd)  is  $f[fd] := [word dword] $m[address]
    ldfsr (address) is FSR := $m[address]
    ld^[c dc]      (address, cd)  is  $c[cd] := [word dword] $m[address]
    ldcsr          (address)      is  CSR := $m[address]
    st^[f df] (fd, address)  is  $m[address] := [word dword] $f[fd]
    stfsr (address)          is  $m[address] := FSR
    st^[c dc] (cd, address)  is  $m[address] := [word dword] $c[cd]
    stcsr (address)          is  $m[address] := CSR
    ldnext(fd, address)  is  ($f[fd] : #64 loc)@loc[0..31] := $m[address]
    stnext(fd, address)  is   $m[address] := ($f[fd] : #64 loc)@bits[0..31]
    -- ldnext(fd, address)  is  $f[fd+1] := $m[address]
    sethi(imm22, rd)  is $r[rd] := bitInsert {wide is 0, lsb is 10} imm22
    [sll srl sra] (rs1, reg_or_imm, rd) is
          $r[rd] := [shl shrl shra](32, $r[rs1], reg_or_imm@bits[5 bits at 0])
    [taddcc taddcctv] (rs1, reg_or_imm, rd) is 
      add_instruction(rs1, reg_or_imm, 0, rd, {set_codes is true})
    [sub subcc subx subxcc] (rs1, reg_or_imm, rd) is 
      subtract_instruction(rs1, reg_or_imm, [0 carryBit], rd, {set_codes is [false true]})
    [tsubcc tsubcctv] (rs1, reg_or_imm, rd) is
      subtract_instruction(rs1, reg_or_imm, 0, rd, {set_codes is true})
    [u s]^div^["" cc] (rs1, reg_or_imm, rd) is
      divide({signed is [false true]}, rs1, reg_or_imm, rd, {set_codes is [false true]})
    fb^[a n u g ug l ul lg ne e ue ge uge le ule o] (target, annul) is
      let rtlop [fba fbn fbu fbg fbug fbl fbul fblg
                 fbne fbe fbue fbge fbuge fble fbule fbo] : #2 bits -> bool
      in [fba fbn fbu fbg fbug fbl fbul fblg fbne fbe fbue fbge fbuge fble fbule fbo] fcc
         --> nPC := target
      end
    rett (address) is 
      let fun restoreOut   n is Reg.out    n := Reg.in' n
          fun restoreLocal n is Reg.local' n := $w[winptr-8 +zx n]
          fun restoreIn    n is Reg.in'    n := $w[winptr-16+zx n]
      in  do8 restoreOut | do8 restoreLocal | do8 restoreIn | winptr := winptr - 16 |
          S := PS | ET := 1 | nPC := address
      end
    t^[a n ne e g le ge l gu leu cc cs pos neg vc vs] (address) is RTL.SKIP
    rd^[y psr wim tbr] (rd) is $r[rd] := [Y PSR WIM TBR]
    wr^[y psr wim tbr] (rs1, reg_or_imm, rd) is [Y PSR WIM TBR] := xor($r[rs1], reg_or_imm)
    stbar () is store_barrier_pending := 1
    unimp (imm22) is RTL.SKIP
    f   ^[s d q]^toi (fs2, fd) is $f[fd] := f2i([word dword qword] $f[fs2],
                                                IEEE754.Round.zero)
    fito^[s d q]     (fs2, fd) is $f[fd] := [word dword qword] (i2f($f[fs2], RD))
    fsto^[d q]       (fs2, fd) is $f[fd] := [dword qword] (f2f(word  $f[fs2], RD))
    fdto^[s q]       (fs2, fd) is $f[fd] := [word qword]  (f2f(dword $f[fs2], RD))
    fqto^[s d]       (fs2, fd) is $f[fd] := [word dword]  (f2f(qword $f[fs2], RD))
    fmovs (fs2, fd) is $f[fd] :=      $f[fs2]
    fnegs (fs2, fd) is $f[fd] := fneg $f[fs2]
    fabss (fs2, fd) is $f[fd] := fabs $f[fs2]
    fsqrt^[s d q] (fs2, fd) is $f[fd] := fsqrt [#32 #64 #128] ($f[fs2], RD)
    f^[add sub mul div]^[s d q]  (fs1, fs2, fd) is
      $f[fd] := [fadd fsub fmul fdiv] [#32 #64 #128] ($f[fs1], $f[fs2], RD)
    fsmuld (fs1, fs2, fd) is $f[fd] := fmulx #32 #64  ($f[fs1], $f[fs2])
    fdmulq (fs1, fs2, fd) is $f[fd] := fmulx #64 #128 ($f[fs1], $f[fs2])
    fcmp ^[s d q] (fs1, fs2) is fcc := fcmp [#32 #64 #128] ($f[fs1], $f[fs2])
    fcmpe^[s d q] (fs1, fs2) is fcc := fcmp [#32 #64 #128] ($f[fs1], $f[fs2])
  -- <incorrect instruction specifications> -- omit
  attribute annul_delay of
    b^[_ _ ne e g le ge l gu leu cc cs pos neg vc vs] (target, annul) is
        let val t is IccTest.tests
        in  (annul <> 0 andalso 
             not ([t.A  t.N   t.NE t.E  t.G   t.LE  t.GE t.L
                   t.GU t.LEU t.CC t.CS t.POS t.NEG t.VC t.VS]))
        end
    [ba bn] (target, annul) is annul <> 0
  attribute trap of
    ld^["" sh uh] (address, rd)  is  alignTrap(address, [4 2 2])
    ldd(address, rd) is
       alignTrap(address, 8) 
       -- second test is incompatible with limited temporaries
       -- | rd@bits[0] <> 0 --> trap(illegal_instruction)
    st^["" h] (rd, address)  is  alignTrap(address, [4 2])
    std       (rd, address)  is
       alignTrap(address, 8)
       -- second test is incompatible with limited temporaries
       -- |  rd@bits[0] <> 0 --> trap(illegal_instruction)
    swap(address, rd) is alignTrap(address, 4)
    jmpl (address, rd) is alignTrap(address, 4)
    ld^[c dc] (address, cd)  is  alignTrap(address, [4 8])
    ldcsr (address)  is  alignTrap(address, 4)
    taddcctv (rs1, reg_or_imm, rd) is 
      (tag_overflows($r[rs1], reg_or_imm) orelse add_overflows($r[rs1], reg_or_imm, 0)
         --> trap(tag_overflow))
    tsubcctv (rs1, reg_or_imm, rd) is
      (tag_overflows($r[rs1], reg_or_imm) orelse sub_overflows($r[rs1], reg_or_imm, 0)
         --> trap(tag_overflow))
    t^[a n ne e g le ge l gu leu cc cs pos neg vc vs] (address) is 
      let val t is IccTest.tests
      in  [t.A  t.N   t.NE t.E  t.G   t.LE  t.GE t.L
           t.GU t.LEU t.CC t.CS t.POS t.NEG t.VC t.VS
          ] --> trap(trap_instruction address@bits[7 bits at 0])
      end
    unimp(imm22) is trap(illegal_instruction)
end