Running on an ubuntu 19.10 host, I believe I'm correctly following the steps in https://github.com/rems-project/sail-arm/tree/master/arm-v8.5-a

The resulting execution of linux runs along for 15 wall clock minutes, and the aarch64 emulator dies due to an exception taken during IFetch. Here's the last few lines of the console log:

0.106016] Floating-point is not implemented

[ 0.106555] Advanced SIMD is not implemented
[ 0.110363] clocksource: jiffies: mask: 0xffffffff max_cycles: 0xffffffff, max_idle_ns: 7645041785100000 ns
[ 0.111487] futex hash table entries: 256 (order: 3, 32768 bytes)
[ 0.139623] vdso: 2 pages (1 code @ ffff000008275000, 1 data @ ffff000008394000)
[ 0.140556] hw-breakpoint: found 2 breakpoint and 2 watchpoint registers.
[ 0.146552] DMA: preallocated 256 KiB pool for atomic allocations
[ 0.147296] Serial: AMBA PL011 UART driver
[ 0.152926] OF: amba_device_add() failed (-2) for /uart@3c000000
[ 0.314280] clocksource: Switched to clocksource arch_sys_counter
[ 0.663831] workingset: timestamp_bits=62 max_order=16 bucket_order=0
[ 0.982486] io scheduler noop registered (default)
[ 1.094483] Serial: AMBA driver
[ 1.098182] cacheinfo: Unable to detect cache hierarchy for CPU 0
[ 1.117508] Warning: unable to open an initial console.
[ 1.119854] Freeing unused kernel memory: 192K
Exception taken during IFetch from PC=0xffff7dfffe7fc400 in cycle=31252682
[Sail] Finished Successfully!

• rm -f bootloader.bin
• rm -f sail.dtb
• rm -f Image
• exit 0
• popd

Hi,

this is a great project which can help me to understand the arm architecture, but when I try to bring up some application on this model, it seems has no trace function which can record all executed instructions and values in related registers or memory, like tarmac trace.
is there any similar function in it and how to enable it?
and does the sail project also support arm v9-A and arm v8-M model?

thanks
Gu

Maybe this should be an issue in the asl_to_sail repo, but I discovered the following today:

The following asl function:

// TGxGranuleBits()
// ================
// Retrieve the address size, in bits, of a granule

integer TGxGranuleBits(TGx tgx)
    case tgx of
        when TGx_4KB  return 12;
        when TGx_16KB return 14;
        when TGx_64KB return 16;

gets translated into the following Sail function:

function TGxGranuleBits tgx = {
    match tgx {
      TGx_4KB => {
          return(12)
      },
      TGx_16KB => {
          return(14)
      },
      TGx_64KB => {
          return(16)
      },
      _ => {
          return(undefined : int)
      }
    }
}

Why does the extra fallback case returning an undefined int get added? The match in the asl code is exhaustive and indeed Sail then complains about it:

Warning: Redundant case src/v8_base.sail:9070.6-7:            ] 7% (1768/24545)          
9070 |      _ => {
     |      ^
     | 
This match case is never used

However, despite the Sail compiler complaining about the case being redundant, the fallback case still exists in the C code. I suspect this is what causes the result of TGxGranuleBits to be a sail_int and the arithmetic that is then performed on the result is also operating on sail_int, not mach_int.

This came up because I am looking into integers that Sail can't prove to fit into machine words in the ARM model, because those are one of the main sources of emulator slowness in my pydrofoil-arm emulator. I can partly fix this on the Pydrofoil side, but maybe it would make sense to fix this more generally? /cc @martinberger

Hello, sorry for bothering you, I'm now working on booting a tiny linux on sail-arm model, the tiny linux is based on Raspberry-Pi-OS, for lesson03, it mainly set up the exception vector table, enable the interrupt controller, and enable the timer, and print something in interrupt handler, but for sail-arm, I'm just wondering how could I enable the timer and interrupt controller so that I could do the samething, I tried the same way to enable timer and set COUNTER_FREQUENCY to cntfrq_el0, but still not working.

In the POL2019 paper, in Sec. 4.2, you describe the following monad:

type monad 'r 'a 'e =
| Done of 'a
| Read_mem of read_kind * address * nat * (list mem_byte -> monad 'r 'a 'e)
| Write_ea of write_kind * address * nat * monad 'r 'a 'e
| Write_memv of list mem_byte * (bool -> monad 'r 'a 'e)
...
| Barrier of barrier_kind * monad 'r 'a 'e
| Read_reg of register_name * ('r -> monad 'r 'a 'e)
| Write_reg of register_name * 'r * monad 'r 'a 'e
| Undefined of (bool -> monad 'r 'a 'e)
| Exception of 'e (* Exception thrown *)

Can you please confirm that the type address denotes physical address (not virtual addresses)?
Also, is that monad transcribed here in Coq?

Is there a way to obtain a C snapshot of the Arm model where the implementation of the monad in the POL2019 paper (sec 4.2, copied below) is user-definable, instead of hard coding the processor state as a struct and specific implementations the monad operations?

type monad 'r 'a 'e =
| Done of 'a
| Read_mem of read_kind * address * nat * (list mem_byte -> monad 'r 'a 'e)
| Write_ea of write_kind * address * nat * monad 'r 'a 'e
| Write_memv of list mem_byte * (bool -> monad 'r 'a 'e)
...
| Barrier of barrier_kind * monad 'r 'a 'e
| Read_reg of register_name * ('r -> monad 'r 'a 'e)
| Write_reg of register_name * 'r * monad 'r 'a 'e
| Undefined of (bool -> monad 'r 'a 'e)
| Exception of 'e (* Exception thrown *)

Doing so would make the C snapshot more generally usable.

It should be possible to write an equivalent model, say machine-word-based-model, where only machine words are used.
The equivalence can be proved by proving functional equivalence of the decode64 functions generated in Coq/isabelle by translating the official model (uses unbounded integers and bitvectors) and the machine-word-based-model model.
How hard would it be to do this? Would the say machine-word-based-model be much more complex?
Doing all this would also provide better C emulators: currently the C translation tries replace unbounded data by machine words, but does not always succeed.

I came across an interesting case today. It seems like “__currentCond” is never set in the ARM model.
This is useful when executing 32-bit instructions that are conditional. In theory, for A32, it should contain the higher bits of the current instruction (28 to 31). But, it is never set in the model.

As a result, the condition attached to an instruction will not be emulated properly. The fix should be to include this in the decoding step. Probably something as simple as: __currentCond = __currentInst[31 .. 28] is a good start (probably not for Thumb though)

For reproducibility and reference, it would be nice if the generated models were labeled with the Arm MRS profile versions they were generated from, e.g. “A-Profile 2023-12” as shown on the download page.

opcode ad{0,4}00400

function memory_pair_simdfp_offset_memory_pair_simdfp_postidx__decode (Rt, Rn, Rt2, imm7, L, V, opc) = {                                                                                                          
    ...                                                                                                                                                                                                      
    let 'scale = 2 + UInt(opc);                                                                                                                                                                                   
    let 'datasize = shl_int(8, scale);                                                                                                                                                                            
    assert(constraint('datasize in {8, 16, 32, 64}));                                                                                                                                                             
    ...                                                                                                                  
}

and similarly for memory_pair_simdfp_preidx_memory_pair_simdfp_postidx__decode but for
opcode ad{8,c}f7c1e
"stp/ldp q30, q31, [x0, #480]!"

Also, shouldn't 'datasize be in 32 and 64 only because UInt(opc) is either 0 or 1?

I would like to get it to be less memory consuming. Do you already know where the bottlenecks are?

Hello, I'm wondering if there are plans to put the Sail version of Arm v9.4a here in the repo?

Hello,

I have noticed that the Sail specification for the USAT instruction (and similar instructions) in the AArch32 instruction set of ARM-v9.4-a seems to differ from the manual.
Referencing this link, there is the following assertion:

    assert(constraint(0 <= 'saturate_to - 1));

This assertion imposes an additional condition, requiring the 'saturate_to variable to be greater than or equal to 1, which is not present in the ARM manual. It appears this was added to prevent accessing a bitvector at index N-1 in the ZeroUnsignedSatQ function.
However, this assertion prevents the valid case from being considered where 'saturate_to is 0. Is there a way to resolve this issue?

Thank you.