Compilation process not ending after pulling the latest version from the repo

[fahadausaf]

Instruction: LDR(literal), Arm v9.4
Target: System Verilog
Sail Version: Build from source (Commit 39ff330)
Issue:

• The compilation process is not terminating for Load/Store instructions after pulling the latest version of code from the repo.
• The process terminates for Data-Processing-Immediate-Instructions after 8 t0 10 minutes which otherwise takes less than a minute when compiled using the release version
• It works fine when the code is compiled to C
• Also noticed that the previous three issues which I reported are not showing up any more in the latest version of the code, i.e. Cannot perform conversion from %vec(%bv64) to %fvec(31, %bv64) #971. Cannot translate literal to SMT: undefined : %bv #906 and Issue with the reverse_endianness() function #884
• The issue persists on both Ubuntu and MacOS

[Alasdair]

Yes, the new SystemVerilog translation I have is much more comprehensive but it can hit a few corner cases where the compilation blows up. Do you have the list of commands you ran to trigger the issue? If I can reproduce it locally it will be much easier for me to diagnose and fix.

[fahadausaf]

Command
sail -sv -no_warn -verbose 4 prelude.sail decode_start.sail builtins.sail v8_base.sail execute.sail decode.sail interface.sail impdefs.sail decode_end.sail main.sail

Files from Arm-Sail v9.4 repo

• prelude.sail
• decode_start.sail
• builtins.sail
• v8_base.sail I am using just a sub-set of v8_base.sail, i.e. list of functions needed for LDR(register-literal)
• interface.sail
• impdefs.sail
• decode_end.sail

Custom Files

• execute.sail
• decode.sail
• main.sail

execute.sail

// execute.sail

val execute_aarch64_instrs_memory_literal_general : forall ('is_signed : Bool) ('nontemporal : Bool) 'size 't ('tagchecked : Bool),
  (0 <= 't & 't <= 31 & 'size in {4, 8}).
  (MemOp, bool('nontemporal), bits(64), bool('is_signed), int('size), int('t), bool('tagchecked)) -> unit

function execute_aarch64_instrs_memory_literal_general (memop, nontemporal, offset, is_signed, size, t, tagchecked) = {
    let address : bits(64) = PC_read() + offset;
    data : bits('size * 8) = undefined;
    let privileged : bool = PSTATE.EL != EL0;
    let accdesc : AccessDescriptor = CreateAccDescGPR(memop, nontemporal, privileged, tagchecked);
    match memop {
      MemOp_LOAD => {
          let data : bits('size * 8) = Mem_read(address, size, accdesc);
          if is_signed then {
              X_set(t, 64) = SignExtend(data, 64)
          } else {
              X_set(t, size * 8) = data
          }
      },
      _ => ()
    };
    ()
}

decode.sail

// decode.sail 

val decode_ldr_lit_gen_aarch64_instrs_memory_literal_general : (bits(5), bits(19), bits(2)) -> unit

function decode_ldr_lit_gen_aarch64_instrs_memory_literal_general (Rt, imm19, opc) = {
    let 't = UInt(Rt);
    memop : MemOp = MemOp_LOAD;
    is_signed : bool = false;
    let nontemporal : bool = false;
    size : {4, 8} = 4;
    match opc {
      0b00 => {
          size = 4
      },
      0b01 => {
          size = 8
      }
    };
    let 'size = size;
    let offset : bits(64) = SignExtend(imm19 @ 0b00, 64);
    let tagchecked : bool = false;
    execute_aarch64_instrs_memory_literal_general(memop, nontemporal, offset, is_signed, size, t, tagchecked)
}

function clause __DecodeA64_LoadStore ((pc, ([bitzero, _, bitzero, bitone, bitone, bitzero, bitzero, bitzero, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _] as __opcode)) if SEE < 624) = {
    SEE = 624;
    let Rt = Slice(__opcode, 0, 5);
    let imm19 = Slice(__opcode, 5, 19);
    let opc = Slice(__opcode, 30, 2);
    decode_ldr_lit_gen_aarch64_instrs_memory_literal_general(Rt, imm19, opc)
}

main.sail

// main.sail

val main : unit -> unit

function main () = {
    print_endline("== initialise ==");

    print_endline("== execute LDR literal ==");

    decode_ldr_lit_gen_aarch64_instrs_memory_literal_general (5^0x01, 0b1000000000000000000, 0b01)
}

[fahadausaf]

Any updates on this issue? @Alasdair