ESBMC intrinsic library

[rafaelsamenezes]

We need a shared header to be used by users. This header should contain all ESBMC instructions that one might need for verifying its programs.

• Depends on #641

[fbrausse]

all ESBMC instructions

If you are referring to the intrinsics as in #653 I would suggest to rather export an interface; maybe equivalent to the current __ESBMC_* but without the inital underscores - make it "a library". Reasons include

• initial __ is reserved to the C implementation, that includes ESBMC's
• maintainability in the future: we may want or need to change both, signature and semantics, of some of those intrinsics in the future
• give this API a version separate from ESBMC in order to communicate incompatible changes (semver or otherwise clearly stated)
• we also might get some macros with a lower-case __esbmc_ prefix in the future
• differences between old and clang frontends

[rafaelsamenezes]

@fbrausse I mostly agree with your comments, I have a few questions though.

give this API a version separate from ESBMC in order to communicate incompatible changes (semver or otherwise clearly stated)

That is a great ideia.

differences between old and clang frontends

IMO we should ignore old frontend. We aren't going to maintain it and we shouldn't help users to use it.

I would suggest to rather export an interface

Could you elaborate on that?

For all other comments related to the __. I was thinking of something like:

// esbmc.h
#pragma once // or equivalent
#ifdef __ESBMC_RUN // we would add this define inside esbmc

extern void *__ESBMC_alloca(size_t size);

#else
#define __ESBMC_alloca(N): assert(!"calling esbmc intrinsic on invalid environment");
#define __ESBMC_assert(C): ; // do nothing

#endif

How would implementing this as a interface be?

[lucasccordeiro]

@rafaelsamenezes: could you please conclude this documentation?

We must replace the malloc calls with __ESBMC_alloca because the latter does not lead to memory leaks and dangling pointers.

[mikhailramalho]

Folks, alloca can lead to unsafe memory accesses. See:

mgadelha@labtop ~ $ cat main.c
#include <stdlib.h>
#include <assert.h>
#include <string.h>

char *foo(size_t buf_size)
{
  char *buffer;
  buffer = (char *) alloca(buf_size);
  memset(buffer, 0, buf_size);
  return buffer;
}

int main()
{
  char* bar = foo(10);
  assert(bar[0] == 0);
  assert(bar[9] == 0);
}

mgadelha@labtop ~ $ gcc main.c -fsanitize=address -O2
main.c: In function ‘foo’:
main.c:10:10: warning: function returns address of local variable [-Wreturn-local-addr]
   10 |   return buffer;
      |          ^~~~~~
In file included from /usr/include/stdlib.h:587,
                 from main.c:1:
main.c:8:21: note: declared here
    8 |   buffer = (char *) alloca(buf_size);
      |                     ^~~~~~

mgadelha@labtop ~ $ ./a.out 
AddressSanitizer:DEADLYSIGNAL
=================================================================
==173759==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x55bbd939516e bp 0x000000000001 sp 0x7fffb5c55c70 T0)
==173759==The signal is caused by a READ memory access.
==173759==Hint: address points to the zero page.
    #0 0x55bbd939516e in main (/home/mgadelha/a.out+0x116e) (BuildId: 54f5b473e57aceba324f9e58731cd5e2a2b079bb)
    #1 0x7ff033a23a8f in __libc_start_call_main ../sysdeps/nptl/libc_start_call_main.h:58
    #2 0x7ff033a23b48 in __libc_start_main_impl ../csu/libc-start.c:360
    #3 0x55bbd9395254 in _start (/home/mgadelha/a.out+0x1254) (BuildId: 54f5b473e57aceba324f9e58731cd5e2a2b079bb)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/home/mgadelha/a.out+0x116e) (BuildId: 54f5b473e57aceba324f9e58731cd5e2a2b079bb) in main
==173759==ABORTING

We need to use either a global object or a static local one here, alloca will not fix this issue.

[lucasccordeiro]

Hi @mikhailramalho,

You're correct. Alloc does not solve the problem. However, __ESBMC_alloca has a different semantic than alloca.

__ESBMC_alloca allocates a memory that is always valid. In particular, __EBMC_alloca was created for users that need a way to initialize byte arrays or to fake register addresses for the harness.

On the one hand, __ESBMC_alloca should not trigger any memory leak or dangling pointer check; it should be equivalent to having a DECL without DEAD. On the other hand, alloca should lead to a dangling pointer, as you pointed out in this issue.

Today morning, I chatted with @fbrausse about this topic; he suggested giving another name to __ESBMC_alloca.

[mikhailramalho]

How about we use a global variable?

From the documentation, we are not allowed to free the get_env return string anyway.

Em qui., 3 de ago. de 2023 às 11:58, Lucas Cordeiro < @.***> escreveu:

Hi @mikhailramalho https://github.com/mikhailramalho,

You're correct. Alloc does not solve the problem. However, __ESBMC_alloca has a different semantic than alloca.

__ESBMC_alloca allocates a memory that is always valid. In particular, __EBMC_alloca was created for users that need a way to initialize byte arrays or to fake register addresses for the harness.

On the one hand, __ESBMC_alloca should not trigger any memory leak or dangling pointer check; it should be equivalent to having a DECL without DEAD. On the other hand, alloca should lead to a dangling pointer, as you pointed out in this issue.

Today morning, I chatted with @fbrausse https://github.com/fbrausse about this topic; he suggested giving another name to __ESBMC_alloca.

— Reply to this email directly, view it on GitHub https://github.com/esbmc/esbmc/issues/652#issuecomment-1664148357, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKEJH4BTU4SZP3I2DUJXMTXTO4DHANCNFSM5RHEZ5FA . You are receiving this because you were mentioned.Message ID: @.***>

--

Mikhail R. Gadelha, Ph.D.

[rafaelsamenezes]

How about we use a global variable?

From the documentation, we are not allowed to free the get_env return string anyway.

Em qui., 3 de ago. de 2023 às 11:58, Lucas Cordeiro < @.***> escreveu:

Hi @mikhailramalho https://github.com/mikhailramalho,

You're correct. Alloc does not solve the problem. However, __ESBMC_alloca has a different semantic than alloca.

__ESBMC_alloca allocates a memory that is always valid. In particular, __EBMC_alloca was created for users that need a way to initialize byte arrays or to fake register addresses for the harness.

On the one hand, __ESBMC_alloca should not trigger any memory leak or dangling pointer check; it should be equivalent to having a DECL without DEAD. On the other hand, alloca should lead to a dangling pointer, as you pointed out in this issue.

Today morning, I chatted with @fbrausse https://github.com/fbrausse about this topic; he suggested giving another name to __ESBMC_alloca.

— Reply to this email directly, view it on GitHub https://github.com/esbmc/esbmc/issues/652#issuecomment-1664148357, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKEJH4BTU4SZP3I2DUJXMTXTO4DHANCNFSM5RHEZ5FA . You are receiving this because you were mentioned.Message ID: @.***>

--

Mikhail R. Gadelha, Ph.D.

That could work for get_env but the main use case is for users having to initialize structs and buffers in their harness.

[mikhailramalho]

That could work for get_env but the main use case is for users having to initialize structs and buffers in their harness.

I see.

~

@lucasccordeiro and @fbrausse given we are changing __ESBMC_alloca to fit this need, we should also drop the define that changes __builtin_alloca to __ESBMC_alloca

[rafaelsamenezes]

That could work for get_env but the main use case is for users having to initialize structs and buffers in their harness.

I see.

~

@lucasccordeiro and @fbrausse given we are changing __ESBMC_alloca to fit this need, we should also drop the define that changes __builtin_alloca to __ESBMC_alloca

The __ESBMC_alloca is defined as __builtin_alloca not the other way around. We can replace it if we ever decide to handle alloca properly.