Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Missing definition of sail_cons with C backend #202

Closed
Timmmm opened this issue Jan 27, 2023 · 16 comments
Closed

Missing definition of sail_cons with C backend #202

Timmmm opened this issue Jan 27, 2023 · 16 comments

Comments

@Timmmm
Copy link
Contributor

Timmmm commented Jan 27, 2023

I cons'd a list... and when I compiled it to C it calls sail_cons():

  sail_cons(&zfoo, zghz360, zfoo);

However this gives a linker error and I can't find the definition of sail_cons anywhere. Am I supposed to write it myself?


On a similar topic, how does garbage collection of lists work? As far as I can tell lists are singly linked and immutable in the FP tradition. So if you do something like this:

list_a = [| 0 |]
list_b = 1 :: list_a
list_c = 2 :: list_a
...
list_a = [| |]
list_b = [| |]
list_c = [| |]

What happens? I can think of a few possibilities:

  1. Lists are always copied, so list_a gets copied into list_b and list_c.
  2. Lists aren't copied, but they are never freed (I hope not!)
  3. List nodes are reference counted.
@Timmmm
Copy link
Contributor Author

Timmmm commented Jan 27, 2023

In fact I don't think it is possible to implement sail_cons() as written. You kind of want this:

#define sail_cons(rop, x, tl) \
    { \
        *(rop) = sail_malloc(sizeof(typeof(**rop))); \
        CREATE(typeof((*rop)->hd))(&((*rop)->hd)); \
        COPY(typeof((*rop)->hd))(&((*rop)->hd), x); \
        (*rop)->tl = tl; \
    }

Unfortunately you can't do that because typeof is a compile time thing so macros don't understand it. The C backend needs to emit something like:

SAIL_CONS(zListElementType)(&zfoo, zghz360, zfoo);

Then I believe this would work:

#define sail_cons(eltype, rop, x, tl) \
    { \
        *(rop) = sail_malloc(sizeof(typeof(**rop))); \
        CREATE(eltype)(&((*rop)->hd)); \
        COPY(eltype)(&((*rop)->hd), x); \
        (*rop)->tl = tl; \
    }

But it might be better if it just generated the code itself rather than resorting to macro mess.

Although... it kind of looks like the code is supposed to do that so I'm not sure what is going on...

@Timmmm
Copy link
Contributor Author

Timmmm commented Jan 27, 2023

Ah wait, it does generate a cons function, like this:

static void zconsz3BlahBlah_RegisterWrite(mylist_pointer *rop, const struct Value x, const mylist_pointer xs) {
  *rop = sail_malloc(sizeof(struct node_mylist_pointer));
  CREATE(Value)(&(*rop)->hd);
  COPY(Value)(&(*rop)->hd, x);
  (*rop)->tl = xs;
}

However it doesn't ever call it. Hmm.

@Timmmm
Copy link
Contributor Author

Timmmm commented Jan 27, 2023

Aha on this line it's checking for "cons" but the function name is actually "sail_cons". I modified it to this:

       | "sail_cons", _ | "cons", _ ->
...

And now it works fine. I was unable to figure out where that extra sail_ is coming from though. Good luck!

@Alasdair
Copy link
Collaborator

Do you have an example program?

@Alasdair
Copy link
Collaborator

Lists are always copied, so list_a gets copied into list_b and list_c.

This is currently how it works but reference counting could also work, and would likely be more efficient.

@Alasdair
Copy link
Collaborator

Should be fixed by c9c8e61

@Alasdair
Copy link
Collaborator

There may be other bugs lurking with the list implementation - I don't think any of our written specs use lists, so at some point this bug got introduced and nobody noticed. I've added a regression test to make sure it doesn't repeat.

@PeterSewell
Copy link
Contributor

PeterSewell commented Jan 27, 2023 via email

@Alasdair
Copy link
Collaborator

Yes I think if we ever do a system verilog or other HDL translation for verification, we will have to forbid usage of linked lists in quite a few places

@Timmmm
Copy link
Contributor Author

Timmmm commented Jan 27, 2023

That was fast! Unfortunately it segfaults for me now:

#0  0x00007ffff6f70e82 in _int_malloc () from /lib64/libc.so.6
#1  0x00007ffff6f72a1e in malloc () from /lib64/libc.so.6
#2  0x00007ffff644379c in sail_malloc ()
   from mycode.so
#3  0x00007ffff64f1e16 in zconsz3z5bv ()
   from mycode.so
#4  0x00007ffff64f7c19 in create_letbind_33 ()

Bit of a strange backtrace. I will investigate on Monday!

For reference, I'm using lists to store a list of memory accesses and register writes (similar to what RVFI-DII does but supporting more than one memory access per instruction).

The alternative is to use platform callbacks, but years of writing Rust has given me a healthy suspicion of callbacks! Especially given that the current C backend is unfortunately fully global.

@Timmmm
Copy link
Contributor Author

Timmmm commented Jan 27, 2023

Ok I got carried away and broke out address sanitiser (it's amazing; if you're not using it you're doing it wrong). Here's the much more helpful output...

❯ ./test.sh 
AddressSanitizer:DEADLYSIGNAL
=================================================================
==87837==ERROR: AddressSanitizer: SEGV on unknown address (pc 0x7fc7ccaf79f2 bp 0x7ffeef5981b0 sp 0x7ffeef598160 T0)
==87837==The signal is caused by a READ memory access.
==87837==Hint: this fault was caused by a dereference of a high value address (see register values below).  Disassemble the provided pc to learn which register was used.
    #0 0x7fc7ccaf79f2 in internal_inc_rc_zz5listz8z5bvz9 /path/to/riscv_sail_model/build/lib/riscv_model.c:101144:24
    #1 0x7fc7ccaf78b1 in zconsz3z5bv /path/to/riscv_sail_model/build/lib/riscv_model.c:101153:3
    #2 0x7fc7ccabf241 in create_letbind_32 /path/to/riscv_sail_model/build/lib/riscv_model.c:101181:5
    #3 0x7fc7ccabd06a in model_init /path/to/riscv_sail_model/build/lib/riscv_model.c:166935:3
    #4 0x7fc7cc614c40 in sail::Model::init() /path/to/riscv_sail_model/build/../lib/riscv_lib.cpp:33:5

The offending code:

static void internal_inc_rc_zz5listz8z5bvz9(zz5listz8z5bvz9 *rop) {
  if (*rop == NULL) return;
  (*rop)->rc = (*rop)->rc + 1;
                      ^---- Error!
  internal_inc_rc_zz5listz8z5bvz9(&(*rop)->tl);
}

Still not obvious to me what is going on tbh. I'll add some printf debugging.

@Timmmm
Copy link
Contributor Author

Timmmm commented Jan 27, 2023

Oh wait here is the error:

static void internal_inc_rc_zz5listz8z5bvz9(zz5listz8z5bvz9 *rop) {
  if (*rop == NULL) return;
  (*rop)->rc = (*rop)->rc + 1;
  internal_inc_rc_zz5listz8z5bvz9(&(*rop)->tl);
}

static void zconsz3z5bv(zz5listz8z5bvz9 *rop, lbits x, zz5listz8z5bvz9 xs) {
  *rop = sail_malloc(sizeof(struct node_zz5listz8z5bvz9));
  (*rop)->rc = 0;
  CREATE(lbits)(&(*rop)->hd);
  COPY(lbits)(&(*rop)->hd, x);
  internal_inc_rc_zz5listz8z5bvz9(&(*rop)->tl);
  (*rop)->tl = xs;
}

You access (*rop)->tl before initialising it. (Can I get a cough Rust? :-D)

@Alasdair
Copy link
Collaborator

Yep, I found that too! ...as well as quite a few more subtle errors.

I wrote some more tests and ran them through valgrind which should hopefully squish most of the bugs.

@Timmmm
Copy link
Contributor Author

Timmmm commented Jan 30, 2023

Unfortunately I still get segfaults with lists in the latest master. I'll see if I can debug it and make a small reproducer.

@Alasdair
Copy link
Collaborator

I can probably work with a larger test case as well if you have one

@Timmmm
Copy link
Contributor Author

Timmmm commented Jan 31, 2023

Ah actually it was my mistake - I forgot to copy the new unsigned int rc; into my header (cough #199 ).

All seems to be working now!

@Timmmm Timmmm closed this as completed Jan 31, 2023
avsm pushed a commit to ocaml/opam-repository that referenced this issue Aug 30, 2023
…_manifest, sail_lem_backend, sail_latex_backend, sail_doc_backend, sail_coq_backend, sail_c_backend, sail and libsail (0.16)

CHANGES:

##### New documentation backend

A new documentation backend for integrating with Asciidoctor has been
added.

##### Automatic formatting (EXPERIMENTAL)

The `sail -fmt` option can be used to automatically format Sail
source. This currently misses some features and can produce ugly
output in some known cases, so is not ready for serious usage yet.

##### Fixes

Various bugfixes including:

* Issue 203: rems-project/sail#203
* Issue 202: rems-project/sail#202
* Issue 188: rems-project/sail#188
* Issue 187: rems-project/sail#187
* Issue 277: rems-project/sail#277

Various mapping issues such as:

* Issue 244: rems-project/sail#244

As well as other minor issues

The `val cast` syntax and support for implict casts is now entirely
removed, as mentioned in the previous release changes. The flags are
still allowed (to avoid breaking Makefiles) but no longer do anything.

The pattern completeness checker has been improved and is now context
sensitive in some cases.
nberth pushed a commit to nberth/opam-repository that referenced this issue Jun 18, 2024
…_manifest, sail_lem_backend, sail_latex_backend, sail_doc_backend, sail_coq_backend, sail_c_backend, sail and libsail (0.16)

CHANGES:

##### New documentation backend

A new documentation backend for integrating with Asciidoctor has been
added.

##### Automatic formatting (EXPERIMENTAL)

The `sail -fmt` option can be used to automatically format Sail
source. This currently misses some features and can produce ugly
output in some known cases, so is not ready for serious usage yet.

##### Fixes

Various bugfixes including:

* Issue 203: rems-project/sail#203
* Issue 202: rems-project/sail#202
* Issue 188: rems-project/sail#188
* Issue 187: rems-project/sail#187
* Issue 277: rems-project/sail#277

Various mapping issues such as:

* Issue 244: rems-project/sail#244

As well as other minor issues

The `val cast` syntax and support for implict casts is now entirely
removed, as mentioned in the previous release changes. The flags are
still allowed (to avoid breaking Makefiles) but no longer do anything.

The pattern completeness checker has been improved and is now context
sensitive in some cases.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants