K-user mailing list

[Robby Findler <robby AT eecs.northwestern.edu>]

Thanks. That's what I was expecting and it is very nice to have it confirmed.

Robby

On Tue, Jan 12, 2016 at 9:26 AM, Dwight Guth <dwight.guth AT runtimeverification.com> wrote:

In response to your question about the third program, what happens is that kcc maintains the type that each object in memory was declared as. Thus, if you try to access an object through a pointer to an incompatible type, it notices that the type of the lvalue is not compatible with the type of the object in memory and reports an error. This is actually part of the rules for effective types that govern aliasing restrictions for malloc'd memory.

On Jan 12, 2016 8:21 AM, "Robby Findler" <robby AT eecs.northwestern.edu> wrote:

Thanks! That's very helpful.

Robby

On Tue, Jan 12, 2016 at 8:18 AM, Rosu, Grigore <grosu AT illinois.edu> wrote:

Thanks for trying kcc out, Robby!

> is it fair to say that the first program I asked about simply exhibits a bug in kcc

Dwight and I had a short discussion about this yesterday and it is likely that you indeed found a bug in kcc.  Actually, a bug in the C semantics.  Dwight was busy yesterday, but the plan is for him to check the details and get back to you.

With real language like C, things can quickly become rather complex.  If you look into the commit history of our C semantics, bugs were fixed at a rate of one or two per week.  This is exactly why we firmly believe that we should build program verifiers based on operational semantics of languages, which we can run and test.  I cannot even imagine how one can maintain a non-executable axiomatic semantics and claim the programs verified with it are indeed correct.  But the ears of our program verification colleagues stay closed to such "non-sense", they continue to develop program verifiers by translating C programs with a nonexistent semantics to a non-executable Boogie blackbox, implementing their translator with thousands of lines of code in their favorite programming language that does not have a semantics itself, and voila: everything works.  Sorry for my sarcasm, it's the PLDI rebuttal time :)

Regarding your new examples below, since the C semantics executes the program, it may hit the same type of undefined behavior at the same line multiple times, from different contexts.  Each of them may be useful to see, because you may fix the problem in the context.  For example, try_it(-2) may have been an error, where you meant try_it(2).  We did implement some support to inhibit reporting the same error in a loop, though, because that can quickly become annoying.  Dwight can give more details.

Regarding your second example below, I should let Dwight, Chris and Chucky give you more proficient answers.

Besides the tools you mentioned, I believe Valgrind can also detect some undefined behaviors, but only a few.  We discussed some of these in our PLDI'15 paper.  BTW, if you want to see all the error codes that kcc is aware of, as well as small programs exercising them, you can take a look at https://github.com/kframework/c-semantics/tree/master/examples/error-codes. These small programs should cover relatively well the spectrum of undefined behaviors of C11.  You can even use these to compare the various tools; you can also catch their false alarms, as we have both bad and good versions of them.

Best,

Grigore

 

 

---

From: Robby Findler [robby AT eecs.northwestern.edu]
Sent: Tuesday, January 12, 2016 6:35 AM
To: Dwight Guth
Cc: Rosu, Grigore; k-user AT cs.uiuc.edu
Subject: Re: [[K-user] ] kcc

Hi Dwight & Grigore: is it fair to say that the first program I asked about simply exhibits a bug in kcc, and not anything fundamental about how it works?

Also I have a few other questions. With this program:

 #include <stdio.h>

 

 int try_it(long i) {

  int a[2]={0x111,0x222};

  int b[2]={0x333,0x444};

  int c[2]={0x555,0x666};

  return b[i];

 }

 int main() {

  printf("0x%x\n",try_it(-1));

  printf("0x%x\n",try_it(2));

 }

kcc seems to produce these 7 messages (I've removed some of the helpful parts of the messages in the interest of brevity):

Error: UB-CEA1

Description: A pointer (or array subscript) outside the bounds of an object.

Error: UB-CEE3

Description: Found pointer that refers outside the bounds of an object + 1.

Error: UB-CER4

Description: Dereferencing a pointer past the end of an array.

Error: UB-CEE2

Description: Indeterminate value used in an _expression_.

Error: UB-CER4

Description: Dereferencing a pointer past the end of an array.

Error: UB-EIO7

Description: Reading outside the bounds of an object.

Error: UB-CEE2

Description: Indeterminate value used in an _expression_.

I can see how the first four messages are somewhat sensible (things kind of go off the rails a bit in this program!) but the last three seem like they are reporting the same things twice. Is that intentional and I'm just not understanding what's going on or is that something you'd rather kcc not produce?

And finally, with this program:

 #include <stdio.h>

 

 void alias(double *f, long *i) {

  *i=0x17;

  *f=0.0;

  printf("0x%lx\n",*i);

 }

 

 int main() {

  long x=0;

  alias((double*)&x,&x);

 }

kcc gives a correct message, but I wonder what it does exactly. In particular, is it maintaining a mapping between all addresses used by the program and the types that that memory has? How fine grained is that mapping? I guess I'm wondering if you can you say a little bit about how this works?

And in case you're curious about why I'm asking all these questions: I co-taught Northwestern's class based on CS:APP in the fall and noticed that the authors of that book don't treat undefined properly. So I spent some time looking into it and playing around with little programs to explain the issues to the students and I'm now looking into tool support that's out there. I know about kcc (obviously) and frama-c and clang's fsanize=undefined. Do you guys know of any other tools in this space worth playing around with?

BTW, kcc is great. Thank you for it!

tia,

Robby

On Sat, Jan 9, 2016 at 10:16 PM, Dwight Guth <dwight.guth AT runtimeverification.com> wrote:

That's an excellent catch with that program. I will look into it on Monday and hopefully have a fix out in less than a day.

On Sat, Jan 9, 2016 at 9:35 PM, Robby Findler <robby AT eecs.northwestern.edu> wrote:

Thanks! I managed to get that to work. I wonder about this program, tho:

 #include <stdio.h>

 unsigned long f() {

  double d = -0.5;

  return d * (1 << 30);

 }

 int main() {

  printf("0x%lx\n",f());

 }

When I run it in kcc, it produces 0x20000000, but I think it is undefined behavior (because it converts a negative double to an unsigned long).

Also, as a more minor note, the vagrant vm seems to be unhappy when it is resumed after suspending (ie on "vagrant resume" after a "vagrant suspend"). It does a bunch of work that appears to be duplicated and then when I login after that, it asks me again for my password and tries to do that same setup step. Cancelling it via control-c seems to get me back to a prompt where I can run kcc again, tho.

Robby

On Sat, Jan 9, 2016 at 3:52 PM, Rosu, Grigore <grosu AT illinois.edu> wrote:

Robby,

If your goal is only to run kcc as is, and not to modify the C semantics, then the simplest way to go is to download the RV-Match tool from https://runtimeverification.com/match/, which already incorporates a fast version of the kcc tool.

Thanks,

Grigore

 

 

---

From: Robby Findler [robby AT eecs.northwestern.edu]
Sent: Saturday, January 09, 2016 3:31 PM
To: Dwight Guth
Cc: k-user AT cs.uiuc.edu
Subject: Re: [[K-user] ] kcc

I wish to run whatever is simple and stable. Apparently I missed a choice point earlier in your documentation. Anyway, what do you recommend?

Thanks,

Robby

On Sat, Jan 9, 2016 at 3:27 PM, Dwight Guth <dwight.guth AT runtimeverification.com> wrote:

You need to be using the latest master of K if you want to build the latest master of the C semantics. :)

On Sat, Jan 9, 2016 at 3:26 PM, Robby Findler <robby AT eecs.northwestern.edu> wrote:

I'm trying to get kcc to build. I think I got as far as the last step
of running "make -j4" in the c-semantics directory, but I get the
error below.

Any hints?

tia,
Robby

☕  make -j4

Building the C parser...

366 states, 5603 transitions, table size 24608 bytes

3239 additional bytes used for bindings

2 shift/reduce conflicts.

2 shift/reduce conflicts.

Makefile:59: .depend-translation: No such file or directory

Makefile:60: .depend-execution: No such file or directory

Makefile:61: .depend-nd: No such file or directory

Makefile:62: .depend-nd-thread: No such file or directory

kdep -d "x86-gcc-limited-libc/c11-nd-thread-kompiled" -I
/Users/robby/git/kframework/c-semantics/x86-gcc-limited-libc/semantics
-- c11.k > .depend-nd-thread

kdep -d "x86-gcc-limited-libc/c11-nd-kompiled" -I
/Users/robby/git/kframework/c-semantics/x86-gcc-limited-libc/semantics
-- c11.k > .depend-nd

kdep -d "x86-gcc-limited-libc/c11-kompiled" -I
/Users/robby/git/kframework/c-semantics/x86-gcc-limited-libc/semantics
-- c11.k > .depend-execution

/bin/sh: kdep: command not found

make[1]: *** [.depend-nd-thread] Error 127

make[1]: *** Waiting for unfinished jobs....

/bin/sh: kdep: command not found

make[1]: *** [.depend-execution] Error 127

/bin/sh: kdep: command not found

make[1]: *** [.depend-nd] Error 127

make: *** [translation-semantics] Error 2

make: *** Waiting for unfinished jobs....