Language improvements to help represent debug info and MORE!

[delcypher]

Boogie currently doesn't allow attributes on all commands (e.g. assignment, goto). There doesn't seem to be a good reason for this. Allowing this would allow debug information to represented in a sane way (currently people just add assume true which is ugly).

[delcypher]

Here is my proposal. The motivation for doing this to allow debug information (i.e. original source information) to be represented in a sane way. I would hope that once these changes are in place we could standardise the way debug information is represented in the Boogie IVL.

Attributes on commands and basic blocks

In this discussion I am only concerned with the unstructured form of Boogie.

Currently you can only have attributes on the following commands

assert {:attribute "foo"}
assume {:attribute "foo"}
call {:attribute "foo"} myfunc();

also it is not possible to but attributes on a basic block. This limitations potentially make it harder to represent debug information. I'd like to propose (informally) the following syntax

goto {:attribute "foo"} <BLOCK> [, <BLOCK> ...];
havoc {:attribute "foo"} <VARIABLE> [, <VARIABLE> ...];
return {:attribute "foo"};
{:attribute "foo"}  <VARIABLE> [, <VARIABLE> ...] := <EXPR> [, <EXPR> ...]

for commands which allows attributes on all commands in the unstructured form of Boogie. The only controversial command is the assign command. I'm not really sure where to put the attribute because the command is infix where as all other commands are prefix. This is my guess but I'd happily change it if there is a good reason to do so.

And for basic blocks something like

entry {:attribute "foo"}:
    assert true;
    goto g1;

g1 {:attribute "bar"}:
    return;

Attribute sets and references

To avoid repetition it would be good to allow common attributes to declared (e.g. a source file name) in one place. I'm imagining global attribute set declarations like so which are in their own namespace.

attr 0 := {:source_file "/path/to/foo.c"}
attr 1 := {@0, :procedure "main"}
attr 2 := {@0, :procedure "comp"}

The @0 means reference the attributes declared in attribute set 0, i.e. the above is equivalent to

attr 0 := {:source_file "/path/to/foo.c"}
attr 1 := {:source_file "/path/to/foo.c", :procedure "main"}
attr 2 := {:source_file "/path/to/foo.c", :procedure "comp"}

As you can see the @ operator references another attribute set and unions it with the set of attributes that the @ occurs in. It would be an error to try to union two attribute sets that contain the same attribute name (even if they are identical). It would also be an error to have a cycle in the references.

IMPLEMENTATION DETAIL: When doing identifier resolution attribute sets would have to be resolved before anything else in the Boogie program and we would need to do so until a fixed point is reached (we would need to detect cycles as this is done).

then these could be referenced like so...

var {@1, :source_line "10", :source_var "g"} g;

procedure main()
{
    var {@1, :source_var "x", :source_line 9} x:int;
    assert {@1, :source_line 10} x > 0;
}

procedure comp()
modifies g;
{
   var {@2, :source_var "y", :source_line 3} y:int;
   {@2, :source_line 4} g := y;
}

This is equivalent to

var {:source_file "/path/to/foo.c", :procedure "main", :source_line "10", :source_var "g"} g;

procedure main()
{
    var {:source_file "/path/to/foo.c", :procedure "main", :source_var "x", :source_line 9} x:int;
    assert {:source_file "/path/to/foo.c", :procedure "main", :source_line 10} x > 0;
}

procedure comp()
modifies g;
{
   var {:source_file "/path/to/foo.c", :procedure "comp", :source_var "y", :source_line 3} y:int;
   {:source_file "/path/to/foo.c", :procedure "comp", :source_line 4} g := y;
}

As you can see using attribute references and sets is much more concise (leading to smaller .bpl files) and readable.

Feedback

This is only a rough sketch of my idea. It probably needs refining so suggestions are welcome. I suspect it would be worth trying to implement some of it to see what parsing issues arise. For example we would need to disallow @ being allowed in a variable/function/procedure/implementation/basicblock name.

[zvonimir]

I like the direction where this is going. My main concern is that in SMACK we use both Boogie and Corral and can easily switch between the two. So we would like to keep their input languages in sync since if they diverge a lot supporting both tools will become a nightmare.

[delcypher]

@zvonimir Initially I don't think the introduction of what I propose (attribute sets, attribute references and attributes supported on all commands and basic blocks) should break many things because Corral uses Boogie's libraries and so when Corral is upgraded to use Boogie's new libraries (with my proposed additions in) it will gain the ability to parse these boogie programs with the new features but still be able to parse old programs (modulo the use of @ in variable names etc...). At this point Corral can continue to use its current way of representing debug information without problems.

However once the proposed features land in Boogie we could use them to define a standard way of representing debug information via attributes. In that case once we decided what this was it would be a very good idea to change Corral to use this new standard.

So what I'm proposing here paves the way for us to define a standard way of representing debug information but right now I'm not trying to define that (the representation of debug info). I'm just trying to get the features in place so that we can do it in the future.

[pdeligia]

All these are nice ideas Dan. I agree that Boogie's support for debug info needs some overhaul. Btw, I am a bit skeptical about the assign command's attribute being at the beginning (i.e. {:attribute "foo"} [, ...] := [, ...]). I wonder if it makes more sense and improves readability to have it in the end or maybe after the := op. But this is just a suggestion.

[delcypher]

@pdeligia I'm also sceptical of where I've placed the attributes for the assign command which is why I'm raising this issue early so we can discuss it. I guess our options are

{:attribute "foo"} x, y := y, x;

x, y {:attribute "foo"} := y, x;

x, y := {:attribute "foo"} y, x;

x,y := y, x {:attribute "foo"};

Something we might want to bear in mind is... what if in the future we want to add attributes to expressions too. In that case only the first two options are usable.

[akashlal]

Hi Dan,
Let me add my 2c.

1. Attributes everywhere: seems reasonable to me.
2. Using attributes on basic blocks to represent debugging information: I
   don't think this is such a good idea. I actually don't see anything wrong
   or ugly about the way debugging information is represented today. I treat
   basic blocks and transfer commands as just control artifacts. Program
   transformations like removing empty basic blocks and coalescing basic
   blocks (done for efficiency and readability) would not be possible if
   blocks or transfer commands carry attributes. Similarly for static
   procedure inlining, if return commands have attributes. Attributes on an
   assume command survives all these transformations, which I like. I think of
   a trace of a sequence of commands (with no control constructs), which is
   why I prefer embedding source information inside a command.

More importantly, I think the job of the compiler would become even harder
if it has to match source information to Boogie control constructs. For
example, in the internal IR that I generate for C, the source information
is already embedded as an IR command. It is more convenient to spit it out
as a Boogie command rather than to start a new basic block.

Of course, none of these are fundamental restrictions, just inertia.

1. Attribute references. I like the fact that collecting repeated
   attributes together in a single reference reduces the memory footprint. Are
   you proposing to hide the attribute references from the user? That is, when
   the Boogie program is parsed in, the references "@1" will get expanded to
   the actual attribute? If so, we only save space on disk, not ram. If not,
   then we need extra logic to read attributes. Further, what happens when you
   Emit a program? Does it emit with attribute references or without?

Akash

On Thu, Apr 23, 2015 at 3:52 AM, Dan Liew notifications@github.com wrote:

@pdeligia https://github.com/pdeligia I'm also sceptical of where I've
placed the attributes for the assign command which is why I'm raising this
issue early so we can discuss it. I guess our options are

{:attribute "foo"} x, y := y, x;

x, y {:attribute "foo"} := y, x;

x, y := {:attribute "foo"} y, x;

x,y := y, x {:attribute "foo"};

Something we might want to bear in mind is... what if in the future we
want to add attributes to expressions too. In that case only the first
two options are usable.

—
Reply to this email directly or view it on GitHub
#5 (comment).

[RustanLeino]

Custom attributes have been useful for a variety of purposes. Allowing them in more places is a good idea.

For commands like goto, havoc, and return, placing the attribute after the keyword (as you have shown, Dan) seems consistent with existing attributes, and the same for basic-block labels. I agree that the assignment statement does not have as obvious a placement. If in the future, we might allow an “attribute command”, which would consist of just an attribute, then placing the attribute at the very beginning of the assignment statement is not a good idea. Like Pantazis, I’m thinking it may be better to place it immediately following the :=. This continues the idea that attributes go after a recognizable token. By the way, if ever place attributes on arbitrary expressions, then placing them after the subexpression denoted may be a fairly good choice, so I propose we don’t put an attribute before the semi-colon of the assignment statement.

(As a remark, attributes, including triggers, on quantifiers go after the ::. This is something I at times have regretted, because this placement seems to go with the body of the quantifier rather than with the quantifier itself or with its bound variables. Indeed, I made the decision differently in Dafny, where attributes go just before the ::.)

Regarding Akash’s concern about program transformations that may destroy attribute information (like on basic blocks and return statements), I think we are already vulnerable to this problem today. For example, assume {:MyAttribute} true; could, in principle, be optimized away by some transformation. I think it seems like a friendly thing to do to allow attributes on, say, basic blocks and return statements, but Boogie users should have the understanding that any transformation (like inlining) that changes the program structure may not be able to preserve attributes or their intended meaning. Is that good enough?

I acknowledge that there can be considerable repetition in some uses of attributes, which invites the design of constructs that reduce such clutter. My opinion, however, is that it’s better to use existing constructs in the language to achieve this. For example, you can declare a constant with an attribute:

const {:source_file “/path/to/foo.c”} attr0: int;

and then reference this constant in other attributes:

{:attr_at attr0}

It would be easy enough to embellish the attributing-finding routines in the Boogie implementation to trace through such :attr_at indirections. Introducing such constants in the Boogie program probably won’t have much performance impact on the SMT solver, but if it becomes an issue, one could introduce yet another attribute like {:attribute_only}, with the meaning that this declaration is to be used only in other attributes and it is omitted from the SMT input. Finally, notice that these existing mechanisms can also allow parameterization, as in:

// declare the attribute shorthand like this:
function {:source_location “/path/to/foo.c”, line} FooLine(line: int): int;

// reference the attribute shorthand like this:
{:attr_at FooLine(218)}

Rustan

[delcypher]

@akashlal

Using attributes on basic blocks to represent debugging information: I
don't think this is such a good idea.

My intention is to allow attributes on basic blocks, whether or not we
should have attributes on basic blocks for debug information is a separate
matter.

I actually don't see anything wrong
or ugly about the way debugging information is represented today.

I don't agree.

From a philosophical perspective using extra assume true; commands to represent debug information feels very wrong to me because a command represents something that a program should execute but assume true; doesn't do anything and so a completely legitimate program transform is to remove these trivial assumes. In my opinion debug information should be annotations on existing statements (i.e. the program commands as if there was no debug information) and should never introduce new commands in a boogie program.

From a practical perspective it is very inefficient in terms of the space used on disk (i.e. for the .bpl file) and in memory.

It also sometimes breaks an optimisation of my tool if there are branches

var x:int;
entry:
   goto thenB, elseB;

thenB:
  assume {:debug_info "bleh"} true;
  assume  x > 0;
  return;

elseB:
  assume {:debug_info "ewwww"} true;
  assume x <= 0;
  return;

My tool tries to look one instruction ahead when it sees a goto and if it sees an assume it considers that to be a branch condition and only creates an execution state if the assume can be satisified. As you can see above inserting an extra assume for debugging information at the beginning of a basic block breaks my optimisation because it looks at the wrong assume. In my tool I avoid this by ripping out all assume true; commands.

I treat
basic blocks and transfer commands as just control artifacts. Program
transformations like removing empty basic blocks and coalescing basic
blocks (done for efficiency and readability) would not be possible if
blocks or transfer commands carry attributes.

Currently I would not expect a program transformation to preserve attributes on basic blocks if they are coalesced. If we decide on a standard way of representing debug information using attributes on commands and basic blocks then ideally all program transforms should preserve these particular attributes if possible. This is not a new problem, for example LLVM represents its debug information using metadata which is attached to commands and program transformations are expected to preserve the debug information.

More importantly, I think the job of the compiler would become even harder
if it has to match source information to Boogie control constructs.
For
example, in the internal IR that I generate for C, the source information
is already embedded as an IR command. It is more convenient to spit it out
as a Boogie command rather than to start a new basic block.

Maybe. I don't envisage putting debug information on basic blocks. I would rather debug information be attached to commands.

Attribute references. I like the fact that collecting repeated
attributes together in a single reference reduces the memory footprint. Are
you proposing to hide the attribute references from the user? That is, when
the Boogie program is parsed in, the references "@1" will get expanded to
the actual attribute?
If so, we only save space on disk, not ram. If not,
then we need extra logic to read attributes.

Ideally I'd like to save space in RAM too so these attribute sets should be a new type of top level declaration in the in memory representation of the boogie program and the attribute references should be preserved (i.e. all references point to the same instance in memory).

Further, what happens when you
Emit a program? Does it emit with attribute references or without?

Ideally when we emit a program the attribute references and sets should be preserved, i.e. the emitted program should be just as compact as the original program.

[akashlal]

I agree that having attributes on block labels, etc. is a good idea.

Regarding debugging information, my intention wasn't to contradict or
reject your proposal. I only wanted to add a perspective on how I designed
my compiler->boogie->verifier frameworks and that I happy with the design :)

Akash

On Fri, Apr 24, 2015 at 1:38 PM, Dan Liew notifications@github.com wrote:

@akashlal https://github.com/akashlal

Using attributes on basic blocks to represent debugging information: I
don't think this is such a good idea.

My intention is to allow attributes on basic blocks, whether or not we
should have attributes on basic blocks for debug information is a separate
matter.

I actually don't see anything wrong
or ugly about the way debugging information is represented today.

I don't agree.

From a philosophical perspective using extra assume true; commands to
represent debug information feels very wrong to me because a command
represents something that a program should execute but assume true;
doesn't do anything and so a completely legitimate program transform is to
remove these trivial assumes. In my opinion debug information should be
annotations on existing statements (i.e. the program commands as if there
was no debug information) and should never introduce new commands in a
boogie program.

From a practical perspective it is very inefficient in terms of the space
used on disk (i.e. for the .bpl file) and in memory.

It also sometimes breaks an optimisation of my tool if there are branches

var x:int;
entry:
goto thenB, elseB;

thenB:
assume {:debug_info "bleh"} true;
assume x > 0;
return;

elseB:
assume {:debug_info "ewwww"} true;
assume x <= 0;
return;

My tool tries to look one instruction ahead when it sees a goto and if it
sees an assume it considers that to be a branch condition and only
creates an execution state if the assume can be satisified. As you can
see above inserting an extra assume for debugging information at the
beginning of a basic block breaks my optimisation because it looks at the
wrong assume. In my tool I avoid this by ripping out all assume true;
commands.

I treat
basic blocks and transfer commands as just control artifacts. Program
transformations like removing empty basic blocks and coalescing basic
blocks (done for efficiency and readability) would not be possible if
blocks or transfer commands carry attributes.

Currently I would not expect a program transformation to preserve
attributes on basic blocks if they are coalesced. If we decide on a
standard way of representing debug information using attributes on commands
and basic blocks then ideally all program transforms should preserve these
particular attributes if possible. This is not a new problem, for example
LLVM represents its debug information using metadata which is attached to
commands and program transformations are expected to preserve the debug
information.

More importantly, I think the job of the compiler would become even harder
if it has to match source information to Boogie control constructs.
For
example, in the internal IR that I generate for C, the source information
is already embedded as an IR command. It is more convenient to spit it out
as a Boogie command rather than to start a new basic block.

Maybe. I don't envisage putting debug information on basic blocks. I would
rather debug information be attached to commands.

Attribute references. I like the fact that collecting repeated
attributes together in a single reference reduces the memory footprint. Are
you proposing to hide the attribute references from the user? That is, when
the Boogie program is parsed in, the references "@1 https://github.com/1"
will get expanded to
the actual attribute?
If so, we only save space on disk, not ram. If not,
then we need extra logic to read attributes.

Ideally I'd like to save space in RAM too so these attribute sets should
be a new type of top level declaration in the in memory representation of
the boogie program and the attribute references should be preserved (i.e.
all references point to the same instance in memory).

Further, what happens when you
Emit a program? Does it emit with attribute references or without?

Ideally when we emit a program the attribute references and sets should be
preserved, i.e. the emitted program should be just as compact as the
original program.

—
Reply to this email directly or view it on GitHub
#5 (comment).

[delcypher]

@RustanLeino

For commands like goto, havoc, and return, placing the attribute after the keyword (as you have shown, Dan) seems consistent with existing attributes, and the same for basic-block labels. I agree that the assignment statement does not have as obvious a placement. If in the future, we might allow an “attribute command”, which would consist of just an attribute, then placing the attribute at the very beginning of the assignment statement is not a good idea. Like Pantazis, I’m thinking it may be better to place it immediately following the :=. This continues the idea that attributes go after a recognizable token. By the way, if ever place attributes on arbitrary expressions, then placing them after the subexpression denoted may be a fairly good choice, so I propose we don’t put an attribute before the semi-colon of the assignment statement.

Sounds sensible

I acknowledge that there can be considerable repetition in some uses of attributes, which invites the design of constructs that reduce such clutter. My opinion, however, is that it’s better to use existing constructs in the language to achieve this. For example, you can declare a constant with an attribute:

const {:source_file “/path/to/foo.c”} attr0: int;

and then reference this constant in other attributes:

{:attr_at attr0}

That's interesting. I guess this has a few advantages

• No syntax change required
• No change to Boogie's current implementation to support referencing other sets of attributes apart from the functions that iterate through attributes.
• You can parametrise attributes (I'm not sure how useful this would be).

But I see several disadvantages to this

• The attribute set names use the same namespace as the global variables which means that a generator of a Boogie program has to take care to avoid clashes. I'd prefer is attribute sets were in their own namespace.
• This could introduce lots of unwanted global variables. This would impact a tool like Corral which tries to abstract away global variables. It would also impact my tool because my tool removes unused (on commands, it ignores uses in attributes) global variables. It would also make the execution state representation for my tool unnecessarily large. However you do mention we could have an {:attribute_only} to avoid this.
• From philosophical view point I want attributes to be a first class citizen in Boogie and adding additional global variables to have "attribute sets" doesn't really fit that view. I'd prefer attribute sets to be a new type of top level declaration and for them to be in their own namespace so that they can only be referenced from within attribute sets. If we use global variables to represent attribute sets then it is legitimate for other parts of the program to use and modify these variables which is not a desirable property.

Admittedly my arguments aren't particularly strong but I'm sure others can chime in with their views on this.