Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000915Frama-CPlug-in > value analysispublic2011-08-05 15:332014-02-12 16:54
Reporterddelmas 
Assigned Toyakobowski 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0000915: interest for a built-in memset function
DescriptionThe following command produces perfectly precise results on the attached example:
frama-c frama-c-lib.c $(frama-c -print-path)/libc.c -val -cpp-command 'gcc -C -E -I$(frama-c -print-path)' -main F1

On the contrary, analysing -main F2 instead of F1 yields unprecise results, unless unrolling is used. It would be of great interest, both for precision and performance, to have a Frama-C built-in for the memset library function, at least in the frequent case where the abstract value of the second parameter is just the {0} singleton.
TagsNo tags attached.
Attached Filesc file icon frama-c-lib.c [^] (334 bytes) 2011-08-05 15:33 [Show Content]

- Relationships

-  Notes
(0002122)
pascal (reporter)
2011-08-05 19:07
edited on: 2011-08-05 23:21

The 0 case is not really harder than other values. 0 repeats every bit. Other values repeats every 8 bits. The span of memory that should be written is a multiple of both 1 and 8 by construction, so it does not really make a difference.

Making a built-in that is as precise as possible (or even just works) for all possible abstract arguments passed to it is extremely difficult because of the variety of abstract values. It's not all "just" intervals, as some people on the internet may dismissively describe the value analysis' abstract values hierarchy.

You can build the use case you'll need implemented by implementing and analyzing with a memset() like this:


void* memset_c (void* dest, int val, size_t len)
{
  unsigned char *ptr = (unsigned char*)dest;
  while (len-- > 0)
    *ptr++ = val;
  return dest;
}

void* memset (void* dest, int val, size_t len)
{
  Frama_C_show_each_memset_args(dest, val, len);
  return memset_c(dest, val, len);
}

Making us implement a built-in that works only for simple arguments will be counter-productive for everyone, as you probably noticed in the case of the memcpy() built-in. We need the entire list of arguments you will be interested in for your project. (We'll assume for the moment that the existing contents for dest do not matter. They do, in fact: if len is not a singleton, they may make the task harder, for instance if they repeat every more than 8 bits)

Then, there is the issue of derived analyses. To make a long story short, when the other analyses (deps, in, out, ...) encounter the Frama_C_memset() built-in, they assume it's a library function because they do not know anything about it (only the value analysis knows about built-ins at this point) and treat it as a library function. This is not always what you might want, especially for a side-effecting built-in. Indeed, you may need a deps-computation Frama_C_memset() built-in if that's the analysis you use, or a out-computation built-in, ...

So what analyses you'll need is something else that we will need to know.

Making the complete built-in that pleases everyone is simply too much work and would stall more important developments.

(0002841)
yakobowski (manager)
2012-04-05 22:44

Surprisingly, we have found that writing a really good memset builtin is even more difficult than writing one for memcpy. A bzero builtin will ship with Nitrogen, with the following restrictions:
- destination must be completely precise
- size must be completely precise

A memset builtin will be available with the commercial version of Frama-C. With a non-zero value for the parameter val, it will actually be more precise than the C version (on top of being considerably faster).

- Issue History
Date Modified Username Field Change
2011-08-05 15:33 ddelmas New Issue
2011-08-05 15:33 ddelmas Status new => assigned
2011-08-05 15:33 ddelmas Assigned To => pascal
2011-08-05 15:33 ddelmas File Added: frama-c-lib.c
2011-08-05 19:07 pascal Note Added: 0002122
2011-08-05 19:07 pascal Note Edited: 0002122
2011-08-05 23:21 pascal Note Edited: 0002122
2012-04-05 22:44 yakobowski Note Added: 0002841
2012-05-19 18:38 svn Checkin
2012-10-23 23:48 yakobowski Assigned To pascal => yakobowski
2012-10-25 14:48 yakobowski Status assigned => resolved
2012-10-25 14:48 yakobowski Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker