... for lem and linksem dependencies.

I added a sail.json file to sail-cheri-mips to try out the new emacs mode https://github.com/CTSRD-CHERI/sail-cheri-mips/blob/master/mips/sail.json but unfortunately it encounters an error:

(message "Checked notrace.sail...")

(message "Checked prelude.sail...")

(message "Checked mips_prelude.sail...")

(message "Checked mips_tlb.sail...")

(message "Checked mips_wrappers.sail...")

(message "Checked mips_ast_decl.sail...")

Internal error: Unreachable code (at "scattered.ml" line 136):
[/local/scratch/rmn30/rems/sail-cheri-mips/mips/mips_insts.sail]:46:0-49
46 |union clause ast = DADDIU : (regno, regno, imm16)
   |^-----------------------------------------------^
   | Found union clause during de-scattering
   | 
   | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues

It works fine in files before mips_ast_decl.sail.

Full error message

Internal error: Unreachable code (at "anf.ml" line 472):
[x.sail]:23:19-26
23 |      ABS(decenc_p(0b0 @ p), rd @ rs)
   |                   ^-----^
   | Could not convert pattern to ANF: ([bitzero, _] as v__3)
   | 
   | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues

Sail version

Sail 0.7.1 (sail2 @ 112f02934f30c631996ff837dd7687039d274e97)

Issue the command with the following test case

sail -c x.sail

default Order dec

$include <prelude.sail>

enum pred = {
  P_false,
  P_true
}

mapping decenc_p : bits(2) <-> pred = {
  0b00 <-> P_true,
  0b01 <-> P_false
}

scattered union ast

val encdec : ast <-> bits(16)
scattered mapping encdec

union clause ast = ABS : (pred, bits(10))

mapping clause encdec =
      ABS(decenc_p(0b0 @ p), rd @ rs)
  <-> 0b10011 @ p : bits(1) @ rd : bits(5) @ rs : bits(5)

end ast
end encdec

val encode : ast -> bits(16)
function encode(x) = encdec(x)

val decode : bits(16) -> ast
function decode(x) = encdec(x)

val "fetch" : unit -> bits(16)

val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
function main () = {
  let bin = fetch();
  let ast = decode(bin);
  let bin' = encode(ast);
  ()
}

The attached test.txt demonstrates problems with the vector_update builtin. Oddly the code type checks OK without a backend but when building c or ocaml I get an error:

./sail -ocaml test.txt
Type error:
No val spec found for vector_update

Also, the C backend appears to be missing an implementation of vector_update_lbits.

While __SetConfig and __ListConfig are undocumented, they're very useful in my RV32 emulator. However, one thing I'd like to do is be able to set multiple configuration values at once in a file, e.g.

debug.disasm_ops=1
cpu.has_ext_m=1
cpu.has_ext_c=0
cpu.has_ext_a=0
cpu.has_ext_f=0

This could be inside the file rv32im-debug.conf, with the simulator being executed e.g.

./build/emu -e build/test.elf --config-file ./rv32im-debug.conf

The semantics would be as if the -C flag was used on the command line multiple times, and config options are applied sequentially (just the same as on the CLI).

This would also dovetail nicely with the ability to read a config file from an environment variable; for example,

export SAIL_EMULATOR_CONFIG=$(pwd)/rv32im-debug.conf
./build/emu -e build/test.elf

But maybe that's not useful unless someone needs it.

When you enter a $ followed by a directive Sail doesn't understand, it seems to get silently ignored. In my case, it was the unfortunate typo:

$incldue <prelude.sail>

I think this is actually a deliberate design to let the Sail preprocessor be agnostic to what directives are supported and let internal modules pick and choose which they want to interpret. It has some awkward side effects for users though. Not sure what can be done about this in the short term, but just wanted to file this in case this behaviour is not actually expected.

test.txt

Type error at no location information available

No kind identifier 'ex5#n

The attached file fails to produce valid ocaml because of a problem with topological sorting:

./sail -ocaml config_fail.sail
+ ocamlfind ocamlc -c -g -package lem -package linksem -package zarith -o out.cmo out.ml
File "out.ml", line 10, characters 20-24:
10 | let zisa_config = ({zISA = true});;
                         ^^^^
Error: Unbound record field zISA
Command exited with code 2.
Compilation unsuccessful after building 6 targets (4 cached) in 00:00:00.
ocamlbuild -use-ocamlfind out.cmo terminated with code 10

The problem goes away if you remove the struct isa_config declaration, so the problem appears to be caused by a conflict between the name of the struct and the name of the top level let binding.

config_fail.sail.txt

cheri128 does not compile to C. Seems to be an issue with the existential type in the call to HighestSetBits, specifically the well-formedness check that occurs there

Minimal example:

default Order dec

$include <flow.sail>
$include <arith.sail>
$include <option.sail>
$include <vector_dec.sail>

val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 .  (int, atom('n)) -> range(0, 'n - 1)

val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range", c: "add_int"} : forall 'n 'm 'o 'p.
  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)

val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)

val min = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)}

overload operator + = {add_range}
overload operator - = {sub_range}

infix 1 >>
infix 1 <<

val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}

val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)

overload operator >> = {shift_bits_right, shiftr}
overload operator << = {shift_bits_left, shiftl}

val HighestSetBit : forall 'N , 'N >= 2. bits('N) -> {'n, 0 <= 'n < 'N . (bool, atom('n))}

function HighestSetBit x = {
  foreach (i from ('N - 1) to 0 by 1 in dec)
    if [x[i]] == 0b1 then return (true, i);
  return (false, 0)
}

/* hw rounds up E to multiple of 4 */
function roundUp(e) : range(0, 45) -> range(0, 48) =
    let 'r = modulus(e, 4) in
    if (r == 0)
    then e
    else (e - r + 4)

function computeE (rlength) : bits(65) -> range(0, 48) =
    let (nonzero, 'msb) = HighestSetBit((rlength + (rlength >> 6)) >> 19) in
    if nonzero then
      /* above will always return <= 45 because 19 bits of zero are shifted in from right */
      {assert(0 <= msb & msb <= 45); roundUp (min(msb,45)) }
    else
      0

val main : unit -> unit effect {escape}

function main() = {
  let _ = computeE(0xFFFF_FFFF_FFFF_FFFF @ 0b1);
  ()
}

test.txt

sail -c test.sail > test.c && gcc -I $SAIL_DIR/lib/ test.c $SAIL_DIR/lib/*.c -lgmp -lz
In file included from test.c:1:0:
test.c: In function ‘recreate_zWARL_range’:
/local/scratch/rmn30/rems/sail2/lib/sail.h:33:24: warning: implicit declaration of function ‘recreate_zz5listz8z5iz9’; did you mean ‘create_zz5listz8z5iz9’? [-Wimplicit-function-declaration]
 #define RECREATE(type) recreate_ ## type
                        ^
test.c:49:60: note: in expansion of macro ‘RECREATE’
 static void RECREATE(zWARL_range)(struct zWARL_range *op) {RECREATE(zz5listz8z5iz9)(&op->zrangelist);}
                                                            ^~~~~~~~
test.c: In function ‘eq_zWARL_range’:
/local/scratch/rmn30/rems/sail2/lib/sail.h:40:21: warning: implicit declaration of function ‘eq_zz5listz8z5iz9’; did you mean ‘copy_zz5listz8z5iz9’? [-Wimplicit-function-declaration]
 #define EQUAL(type) eq_ ## type
                     ^
test.c:54:10: note: in expansion of macro ‘EQUAL’
   return EQUAL(zz5listz8z5iz9)(op1.zrangelist, op2.zrangelist);
          ^~~~~
/tmp/ccWuM7h2.o: In function `recreate_zWARL_range':
test.c:(.text+0x22a): undefined reference to `recreate_zz5listz8z5iz9'
/tmp/ccWuM7h2.o: In function `eq_zWARL_range':
test.c:(.text+0x270): undefined reference to `eq_zz5listz8z5iz9'
collect2: error: ld returned 1 exit status

The sail mappings support for hexadecimal strings requires builtin functions hex_bits_N_matches prefix for every N where N is the length of a bitvector mapped to a hexadecimal string in a mapping.
Quite a few of these are implemented in the library for ocaml, lem and coq but not for C. This can lead to generated C that does not compile.

A difficulty in implementing them is that the type of hex_bits_N_matches_prefix is string -> option(bits(N), nat)) and option is not a primitive type in sail (or C). This prevents #57 from completely fixing this issue without changes to the way mappings work.

The attached file contains a struct declaration followed by an instantiation that does not define all of the fields. Sail does not complain but ocaml bombs on the resulting ml:

 ./sail -ocaml struct_val.sail
+ ocamlfind ocamlc -c -g -package lem -package linksem -package zarith -o out.cmo out.ml
File "out.ml", line 14, characters 15-44:
14 | let zfoo_val = ({za = (Big_int.of_int (1))});;
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Some record fields are undefined: zb
Command exited with code 2.
Compilation unsuccessful after building 6 targets (4 cached) in 00:00:00.
ocamlbuild -use-ocamlfind out.cmo terminated with code 10

struct_val.sail.txt

I recognize that this is surely not a huge priority, but:

lib/int128/sail.c and lib/sail.c each make use of X86-specific built-ins and __attribute__((target ("bmi2"))). This means that the resulting C translations are necessarily post-Haswell X86 only, which is not great (though one assumes the performance gain from BMI2 for bit twiddling is considerable).

Hi!
At first, I am a newbie in Ocaml etc. and I try to build SAIL on my Debian 10 with Ocaml 3.05.

I followed the instructions of the INSTALL.md

It stops at Sail itself and says:
File "sail.ml", line 448, characters 8-18:
Error: Unbound module B64
Command exited with code 2.

Due to an API break in the module base64, I changed the version of base64 from 3.2.0 to 2.3.0 and try to build it again:
File "jib/jib_smt.ml", line 774, characters 19-28:
Error: Unbound value List.init
Command exited with code 2.

Now, I have no idea how to handle it. I guess some API changes causes this errors and make the install instruction be invalid. Any ideas?

I was surprised recently to find that sail silently permits access to invalid vector indices e.g.:

test1.txt

The resulting ocaml executable crashes with Exiting due to uncaught exception but the C one appears to exit successfully...

For including sail in ISA documentation it would be useful to have a latex backend with the following features:

1. Ability to attach doc-comments to functions / function clauses / val declarations.
2. Dump each function / clause / declaration to a separate latex file so they can be included at convenient places in documentation.
3. Include hyperrefs from function uses to definitions.

It's probably OK if the formatting is canonicalised and any inline comments are lost, but definitely want to dump before desugaring.

I don't know if sail2 is meant to be considered unstable at this point, but using commit 5744317 I'm experiencing the following:

$ cat test.sail
default Order dec
$include <prelude.sail>

infix 9 :=

val main : unit -> unit effect {wreg}
function main() = {
  (*x) := 0xcafebeef
}
$ sail test.sail
Internal error: Unreachable code (at "initial_check.ml" line 414):
[test.sail]:8:3-5
8 |  (*x) := 0xcafebeef
  |   ^^
  | Unparseable construct in to_ast_exp
  |
  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues

The spec is kind of nonsense, but I was not expecting an ICE.

Apart from this, my experience with Sail has so far been very positive. Very nice work :)

Not sure if this is a known issue. The execute function on ITYPE in riscv/riscv_duopod.sail is defined as follow:

function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
  ... // function body

The pattern requires the fourth argument to be RISCV_ADDI. However, the Coq translation of this function does not reflect that, it is defined as follow:

Definition execute_ITYPE  (imm : mword 12) (rs1 : mword 5) (rd : mword 5) (RISCV_ADDI : iop)  
: M (unit):= ... (* function body *)

The RISCV_ADDI identifier here is just a parameter.

ln the opam sail install instructions here:

https://github.com/rems-project/sail/wiki/OPAMInstall

"opam switch 4.06."

should be changed to

"opam switch create 4.06.1"

This is the error I am getting when trying to compile sail-arm with the latest sail (sail2 branch)

../../sail/sail -c -Oconstant_fold -non_lexical_flow -no_lexp_bounds_check -memo_z3 -no_warn -dno_cast  model/prelude.sail model/no_devices.sail model/aarch_types.sail model/aarch_mem.sail model/aarch64.sail model/aarch64_float.sail model/aarch64_vector.sail model/aarch32.sail model/aarch_decode.sail model/elfmain.sail
Type error:
[model/aarch_mem.sail]:2432:0-2450:1
2432 |function GTESetPPURegion () = {
     |^------------------------------
2450 |}
     |^
     | Effects do not match: {rreg, undef, wreg} declared and {escape, rreg, undef, wreg} found
     | 

In the paper (sail-popl2019), it mentions that the translation to Coq is completed only for MIPS. I wonder, currently whether the translation for arm v8 is available or not.

This file contains a missing ' on x in the definition of foo and sail reports an error when calling z3:

bug.txt

Error when calling smt: Reporting.Fatal_error(_)

Interestingly if the ' is missing from definition of x but present for foo it gives a different error about the call to sail_zeros.

While trying to test sail I tried the

A trutorial RISCV example : riscv_duopod.sail

as shown on the manual chapter 2. It does not work out of the box.
for instance when I tried type checking riscv_duopod.sail,
type regbits = bits(5) throws an error

could not find type constructor bits
and option(ast) throws an error

could not find type constructor option

after manually adding ./lib/vector_dec.sail and ./lib/option.sail it throws an error

Type error. No default order has been set

It would be very helpful to provide an out of the box tutorial example

Both lookup_sym and load_elf in the runtime system use gzopen to read the specified input ELF files. This works fine, because gzopen can seamlessly read non-gzip files without issue, making it a single code path to read both. I assume the support is here so you can basically boot gzip'd ELF files that might be produced by OS build systems or somesuch.

However, when cross compiling my generated C code to WebAssembly, gzip is a fairly heavy dependency to support and cross compile itself, and being able to drop it would be nice.

If you wanted to keep existing models working seamlessly without adding any new APIs to the C subsystem -- it'd probably be better to opt-out of gzip support, rather than opt-in, at C compile time, i.e. a -DNO_GZIP=1 when compiling the C files will turn it off, but otherwise it will be on by default.

Alternatively, load_elf and lookup_sym could be changed to split out the gzip decompression part (perhaps by offering bindings to gzip in the stdlib or something, or a separate load_compressed_elf etc functions, and models would use a check like is_gzipped(...) to check which function to call.)

I know there's a whole different Makefile-build-system for Coq (as used by BBV) but at least for this Makefile, the following rule can end up rebuilding .vo files in other directories:

E.g. Sail2_instr_kinds.v depends on bbv/Word.vo, but instead of using that file, it'll rebuild from Word.v (this can be seen with make --dry-run).

Should I change it to

$(TARGET):%.vo: %.v

Or is there a more conventional Coq-Makefile-build coming?

test.sail:

val foo : unit -> unit
function foo () = ()
function foo () = ()

../sail -ocaml test.sail 
+ ocamlfind ocamlc -c -package lem -package linksem -package zarith -o out.cmo out.ml
File "out.ml", line 6, characters 4-8:
Error: Variable zfoo is bound several times in this matching
Command exited with code 2.
Compilation unsuccessful after building 4 targets (3 cached) in 00:00:00.

Hi,
I'd like use sail to model implicit state of the hardware to augment execution with "side-channel leakages" e.g. last memory write, computation results, state updates, etc. . This is needed to implement a dedicated "leaky execution" to produce a modelled trace of leakages which occur during execution on real hardware.

It seems that monads are specified in the ott lang specification - adding state there will likely break things down the chain, right? What is a good approach to add additional state to keep track of "side-channel state"?
I'm not even sure if this needs to be done within sail or if it is better to implement it somewhere in the ML/C backends/main/etc. .

Sail looks really promising but very likely I am not entirely understanding how it works :)

For example when compiling the attached file which contains a reference to a non-existent built-in function:

./sail -ocaml test.txt                                                      
Generating main
+ ocamlfind ocamlc -c -package lem -package linksem -package zarith -o out.cmo out.ml
File "out.ml", line 4, characters 55-59:
Error: Unbound value asdf
Command exited with code 2.
Compilation unsuccessful after building 7 targets (0 cached) in 00:00:00.
cp: cannot stat 'main.native': No such file or directory
[rmn30@ideo .../rems/sail2]$ echo $?
0

test.txt

Sorry, another one from me... I reduced a problem I'm having to this:

$ cat test.sail
default Order dec
$include <prelude.sail>

let THIRTY_TWO : atom(32) = 32

val f : bits(32) -> bits(THIRTY_TWO)
$ sail -o test -lem -lem_mwords test.sail
$ lem -isa -outdir . -lib Sail=.../share/src/lem_interp -lib Sail=.../share/src/gen_lib test.lem test_types.lem
File "test.lem", line 55, character 25:
  Syntax error

The area of the file Lem is complaining about looks like this:

 53 | let (THIRTY_TWO : integer) = (32:ii)
 54 |
 55 | val f : Size 'THIRTY_TWO => mword ty32 -> mword 'THIRTY_TWO
 56 |

To give some context for my nonsense, what I was originally attempting was to define a bitfield, one field of which is a slice whose range is dependent on a constant defined elsewhere. I want to be able to edit one place (the constant) to then affect several parameterised data structures. I figured out that my constant had to be an atom which means I awkwardly need to give the value of it twice, but it still isn't usable as the bound of a bit slice. Using it in other places like the above makes me think I'm doing something wrong.

I know that the x86 spec is out of date, but I thought I'd mention this since this stuff is not easy to find... According to the reference manual, opcode 0x83 performs a binop on r/m16/32/64 and imm8, while 0x81 does a binop with r/m16/32/64 and imm16/32. Currently, 0x81 and 0x83 are being decoded to the same AST, the imm16/32 version. I think L1148 should read (imm, strm4) = immediate8 (strm3) instead of using oimmediate (sz, strm3).

type tuparg = (int, int)

union Bar = {
      X : tuparg
}

Gives:

Type error at no location information available

Function X not applied to enough arguments

I don't understand much of SAIL, but I think the manual has a typo on pg. 12, Section 4.3.
"The type int('o) is an integer
exactly equal to the Int-kinded type variable 'n,"

'n should probably be 'o.

Also, you should make it clear that your definition of the natural numbers (nat) includes 0.

The following code fragment:

function rX 0 = EXTZ(0x0)
and rX (r if r > 0) = Xs[r]

in sail-riscv/model/riscv_duopod.sail triggers the following error:

Internal error: Unreachable code (at "jib/anf.ml" line 516):
[riscv_duopod.sail]:22:12-13
22 |function rX 0 = EXTZ(0x0)
   |            ^
   | Could not convert pattern to ANF: 0
   | 
   | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues

when compiled with the following command line:

sail -c prelude.sail riscv_xlen64.sail riscv_duopod.sail

The version of Sail I'm using is:

Sail 0.9 (sail2 @ opam)

On the other hand, neither "sail" without option nor "sail -ocaml" fails on the above code fragment.

Also, the following code fragment:

function rX r =
if r == 0 then EXTZ(0x0) else Xs[r]

compiles for all three options.

The riscv/prelude.sail file defines the bits data type as follow:

type bits ('n : Int) = vector('n, dec, bit)

What is the reason that Int is chosen here instead of Nat?

With the possible presence of negative numbers, the following definition also becomes problematic:

val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))

If o is a nagative number, the vector returned by this operation may be even bigger than n, the length of the original vector. Is this intended?

The CHERI model is currently failing to build for ocaml due to a bug in code generation. I minimised the code to this example:

test.txt
out.txt

The problem is that the generated ocaml uses undefined_CapStruct in the initialisation of KCC before it is declared. It appears to be confused by the fact that SignalException is declared and used (in SignalExceptionBadAddr) before it is defined so it generates a recursive set of ocaml functions even though there is no recursion going on. The problem would be solved if sail emitted undefined_CapStruct just after the definition of zCapStruct where string_of_zCapStruct is defined.

The Sail mode would be very useful to have more widely available. MELPA is a very good way to do this; I use it for my own cryptol-mode.

However, this requires adding metadata: see #29 for that.

Once that's in place, I believe we can simply do add a MELPA recipe upstream, like:

(sail2-mode
  :fetcher github
  :repo "rems-project/sail"
  :files ("editors/*.el"))

And then anyone can use the Sail mode in recent Emacs by adding MELPA as an upstream (and this will normally happen by default with Spacemacs, DOOM Emacs, etc)

It's not possible to write a zero length vector literal in sail at the moment e.g.:

let x : bits(0) = []

gives a syntax error on the closing ]. As a workaround it's possible to use the sail_zeros builtin:

let x : bits(0) = sail_zeros(0)

The check here for w < q should be w <= q, because q == w is also unrepresentable.

I'm trying to get Sail to generate C code for an Armv8 model, but I can't seem to get it to work for any of the provided ones. I've tried installing v0.10 from the OPAM repository as well from the head of the sail2 branch.

The README indicates that the hand-written model that comes with the repository is out-of-sync with the latest Sail, and indeed I get an error when trying to use it:

$ sail -c arm/armV8.sail 
Syntax error:
[arm/armV8.sail]:1:0-0
1 |(*========================================================================*)
  |^
  | current token: (

So, I then tried the automatically generated Armv8.5 model that comes in a separate repository, but I get a different error this time:

$ sail models/arm/arm-v8.5-a/model/aarch64.sail 
Lexical error:
[models/arm/arm-v8.5-a/model/aarch64.sail]:3326:34-34
3326 |    let msg : string = "Prefetch" ++ " address=0x" ++ HexStr(UInt(address)) ++ " op=" ++ op ++ " target=" ++ target ++ " stream=" ++ stream;
     |                                  ^
     | Operator fixity undeclared ++

I have zero experience with OCaml so can't tell if there's a real issue here or if I'm just doing something wrong.

Can you give some guidance on how to get any version of Sail working with any Armv8 model? At this stage I just want to see the C code that it will generate for instruction decoding and execution, to see if I might be able to modify it to make use of for my own work.

e.g.

val foo : unit -> unit

val bar : unit -> unit
function bar () = foo ()

register x : int

function foo () = ()

../sail -ocaml test.sail                                                   
+ ocamlfind ocamlc -c -package lem -package linksem -package zarith -o out.cmo out.ml
File "out.ml", line 4, characters 54-58:
Error: Unbound value zfoo
Command exited with code 2.
Compilation unsuccessful after building 4 targets (2 cached) in 00:00:00.

Note that if the register definition is not present foo and bar are emitted as a pair of mutual recursive functions, which works as expected OK.

Hi!
I want to convert the sail file to a lem file. For example, I executed the command sail -lem -o test -lem_mwords -lem_lib test_extras prelude.sail no_devices.sail aarch_types.sail aarch_mem.sail aarch64.sail aarch64_float.sail aarch64_vector.sail aarch32.sail aarch_decode.sail in the sail-arm/model folder. but a type error occurs, i.e.,
Type error:
[aarch_mem.sail]:2444:4-28
2444 | _GTE_PPU_Address[region] = _GTEParam[1];
| ^----------------------^
| Vector assignment not provably in bounds _GTE_PPU_Address[region]
| This error occured because of a previous error:
| [aarch_mem.sail]:2444:4-28
| 2444 | _GTE_PPU_Address[region] = _GTEParam[1];
| | ^----------------------^
| | Vector assignment not provably in bounds _GTE_PPU_Address[region]
|
I don't know if the conversion method is wrong, or how should I convert the sail to lem? look forward to your reply, thank you.

union exception = {E : unit }

val foo : forall ('o : Type) . unit -> 'o effect {escape}
function foo () = throw E

val bar : unit -> int effect {escape}
function bar () = foo()

val baz : unit -> string effect {escape}
function baz () = foo()

../sail -ocaml test.sail 
+ ocamlfind ocamlc -c -package lem -package linksem -package zarith -o out.cmo out.ml
File "out.ml", line 13, characters 33-61:
Error: This expression has type Big_int.num = Big_int_impl.BI.big_int
       but an expression was expected of type string
Command exited with code 2.
Compilation unsuccessful after building 4 targets (2 cached) in 00:00:00.

bar or baz on its own is OK but having both causes error because ocaml infers foo to have either int or string return type.

version

Sail 0.8 (sail2 @ 2b0a4e2746e632d3f823baade49b560f79317497)

test case

$include <prelude.sail>

function main () : unit -> option(unit) = {
  match Some(()) {
    Some(_) as x => x,
    _ => None()
  }
}

sail test.sail -c

I am building Sail on a new Ubuntu 18.04.4 LTS (x86_64) system and I am getting the following error:
I have used opam 1.2 and had similar error then I moved to opam 2.0 (this).
Similar build error with ocaml 4.06.1...
(I tried quite a few configurations....)

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of ocaml failed at "/gpfs/haifa-h6/00/shvadron/.opam/opam-init/hooks/sandbox.sh build ocaml
/gpfs/haifa-h6/00/shvadron/.opam/4.07.0/share/ocaml-config/gen_ocaml_config.ml 4.07.0 ocaml".

ERROR while compiling ocaml.4.07.0
context 2.0.4 | linux/x86_64 | base-bigarray.base base-threads.base base-unix.base ocaml-base-compiler.4.07.0 | https://opam.ocaml.org/#23c4663f
path /gpfs/haifa-h6/00/shvadron/.opam/4.07.0/.opam-switch/build/ocaml.4.07.0
command /gpfs/haifa-h6/00/shvadron/.opam/opam-init/hooks/sandbox.sh build ocaml /gpfs/haifa-h6/00/shvadron/.opam/4.07.0/share/ocaml-config/gen_ocaml_config.ml 4.07.0 ocaml
exit-code 1
env-file /gpfs/haifa-h6/00/shvadron/.opam/log/ocaml-28951-ad8886.env
output-file /gpfs/haifa-h6/00/shvadron/.opam/log/ocaml-28951-ad8886.out
output
OCaml version mismatch: 4.05.0, expected 4.07.0

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
\u250c\u2500 The following actions failed
\u2502 \u03bb build ocaml 4.07.0
\u2514\u2500
\u2576\u2500 No changes have been performed

May be I should start from scratch? How?

If you try to run make -C cheri latex_256 in sail-cheri-mips repository using latest HEAD the resultant latex has two problems:

1. The commands.tex file defines \sailvalabsInt twice, resulting in a latex error
2. Other .tex files contain useless text like this:

    |                ^-------------------------------
281 |}
    |^
    |

Hi,
sail is awesome, the aarch64 work appears to be the most comprehensive framework around :)
Is support for the Arm M profiles for microcontrollers planned or ongoing?
I was wondering how much effort it is to implement asm/elf decoders and a simplified AST for it (A32, T32 + regs + execute - no mmu/interrupt). Maybe most of it is already available from aarch64?

KR
Marc

val print_int = "print_int" : (string, int) -> unit

val main : unit -> unit
function main () = {
  foreach(i from 0 to 3) {
    print_int("i=", i);
  }
}

Generated ocaml for above prints 0 to 2 i.e. foreach loop is not inclusive of end point. This is a change form sail1 which was inclusive. Lem generation fails for this test so can't compare.

Last few lines of opam output:

λ compiled  sail.0.7
+ /local/scratch/alr48/cheri/output/sdk/opamroot/opam-init/hooks/sandbox.sh "install" "make" "INSTALL_DIR=/local/scratch/alr48/cheri/output/sdk/opamroot/4.06.0" "SHARE_DIR=/local/scratch/alr48/cheri/output/sdk/opamroot/4.06.0/share/sail" "install" (CWD=/local/scratch/alr48/cheri/output/sdk/opamroot/4.06.0/.opam-switch/build/sail.0.7)
- if [ -z "/local/scratch/alr48/cheri/output/sdk/opamroot/4.06.0/share/sail" ]; then echo SHARE_DIR is unset; false; fi
- mkdir -p /local/scratch/alr48/cheri/output/sdk/opamroot/4.06.0/bin
- cp src/isail.native /local/scratch/alr48/cheri/output/sdk/opamroot/4.06.0/bin/sail
- mkdir -p /local/scratch/alr48/cheri/output/sdk/opamroot/4.06.0/share/sail
- make -C lib/isabelle all
- make[1]: Entering directory '/local/scratch/alr48/cheri/output/sdk/opamroot/4.06.0/.opam-switch/build/sail.0.7/lib/isabelle'
- make[1]: opam: Command not found
- Makefile:12: *** isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable. Stop.
- make[1]: Leaving directory '/local/scratch/alr48/cheri/output/sdk/opamroot/4.06.0/.opam-switch/build/sail.0.7/lib/isabelle'
- Makefile:16: recipe for target 'install' failed
- make: *** [install] Error 2
[ERROR] The installation of sail failed at "make INSTALL_DIR=/local/scratch/alr48/cheri/output/sdk/opamroot/4.06.0
        SHARE_DIR=/local/scratch/alr48/cheri/output/sdk/opamroot/4.06.0/share/sail install".

Reverting 365cf20 makes it install again for me.

I'm not sure why it can't find opam, if I add an env call before it lists my opam install directory in PATH.

In sail2 if you define a field with the same name in two different bitfield types then the generated accessor functions (_get_fieldname) collide. The resulting error message is not very friendly e.g. when porting the mips spec I got the error:

Identifier _get_BadVPN2 is already bound

If we want to support duplicate field names we should include the name of the bitfield type in the generated accessor function, otherwise we should produce a friendly error message.

The following code (reduced from MIPS spec) produces an assertion failure:

union option ('a : Type) = {None, Some : 'a}

union ast = {Foo : unit}

let x : option(ast) = Some(Foo)

let y : unit = match(x) {
  Some(Foo) => (),
  Some(a)   => (),
  None      => ()
}

The error is:
Fatal error: exception File "pattern_completeness.ml", line 236, characters 10-16: Assertion failed