llvm dev - Mar 2010 - [LLVMdev] Changes between 2.6 and 2.7: SSA Verifier and visitFreeInst

Hi llvm,

1) The lib/VMCore/Verifier.cpp in 2.7 implements Verifier::VerifyType,
which is empty in 2.6. I noticed that it does not check all types,
for example, UnionTyID, OpaqueTyID, LabelTyID, MetadataTyID
and etc are ignored in the 'default' branch. Does it mean we dont
need to check them?

Another question is: How much does Verifier.cpp check statically?
Can I take it as a type checker for SSA? Is there any static
semantics that has not been checked yet?

2) visitFreeInst has been removed from lib/ExecutionEngine/Interpreter in 2.7
Will this have any back-compatible problem when interpreting any
*.bc from 2.6?

Thanks
-- 
Jianzhou

On Mar 6, 2010, at 9:13 AM, Jianzhou Zhao wrote:
> Hi llvm,
> 
> 1) The lib/VMCore/Verifier.cpp in 2.7 implements Verifier::VerifyType,
> which is empty in 2.6. I noticed that it does not check all types,
> for example, UnionTyID, OpaqueTyID, LabelTyID, MetadataTyID
> and etc are ignored in the 'default' branch. Does it mean we dont
> need to check them?
They are leaf types (just like integer type), there is nothing to check.
> Another question is: How much does Verifier.cpp check statically?
> Can I take it as a type checker for SSA? Is there any static
> semantics that has not been checked yet?
The verifier is best effort, it does not guarantee correctness.
> 2) visitFreeInst has been removed from lib/ExecutionEngine/Interpreter in
2.7
> Will this have any back-compatible problem when interpreting any
> *.bc from 2.6?
The .bc reader will eliminate freeinst from the ir when reading an old file.

-chris

Jianzhou Zhao wrote:
> Hi llvm,
>
> 1) The lib/VMCore/Verifier.cpp in 2.7 implements Verifier::VerifyType,
> which is empty in 2.6. I noticed that it does not check all types,
> for example, UnionTyID, OpaqueTyID, LabelTyID, MetadataTyID
> and etc are ignored in the 'default' branch. Does it mean we dont
> need to check them?
We do need to check union. I'll add that. The others don't need a case 
because they don't contain subtypes; it's impossible to have an illegal 
label type. It's either a label type or it isn't. :)
> Another question is: How much does Verifier.cpp check statically?
> Can I take it as a type checker for SSA? Is there any static
> semantics that has not been checked yet?
There are things that it does not check yet. It doesn't verify constant 
expressions, so 'bitcast i32* @x to i32' will still escape detection, if
you can manage to create one (ie., you're running with assertions off).

Further, there are semantics of the program that the verifier will never 
verify. It is undefined behaviour to shift beyond the width of an 
integer. It is undefined behaviour to call a function with mismatching 
calling conventions. http://llvm.org/docs/FAQ.html#callconvwrong
> 2) visitFreeInst has been removed from lib/ExecutionEngine/Interpreter in
2.7
> Will this have any back-compatible problem when interpreting any
> *.bc from 2.6?
The 'free' instruction has been removed from LLVM 2.7. Any .bc files 
using it will have a 'call @free' inserted in its place.

Nick

On Sat, Mar 6, 2010 at 2:35 PM, Nick Lewycky <nicholas at mxc.ca>
wrote:
> Jianzhou Zhao wrote:
>>
>> Hi llvm,
>>
>> 1) The lib/VMCore/Verifier.cpp in 2.7 implements Verifier::VerifyType,
>> which is empty in 2.6. I noticed that it does not check all types,
>> for example, UnionTyID, OpaqueTyID, LabelTyID, MetadataTyID
>> and etc are ignored in the 'default' branch. Does it mean we
dont
>> need to check them?
>
> We do need to check union. I'll add that. The others don't need a
case
> because they don't contain subtypes; it's impossible to have an
illegal
> label type. It's either a label type or it isn't. :)
>
>> Another question is: How much does Verifier.cpp check statically?
>> Can I take it as a type checker for SSA? Is there any static
>> semantics that has not been checked yet?
>
> There are things that it does not check yet. It doesn't verify constant
> expressions, so 'bitcast i32* @x to i32' will still escape
detection, if you
> can manage to create one (ie., you're running with assertions off).
>
> Further, there are semantics of the program that the verifier will never
> verify. It is undefined behaviour to shift beyond the width of an integer.
> It is undefined behaviour to call a function with mismatching calling
> conventions. http://llvm.org/docs/FAQ.html#callconvwrong
>
>> 2) visitFreeInst has been removed from lib/ExecutionEngine/Interpreter
in
>> 2.7
>> Will this have any back-compatible problem when interpreting any
>> *.bc from 2.6?
>
> The 'free' instruction has been removed from LLVM 2.7. Any .bc
files using
> it will have a 'call @free' inserted in its place.
Thanks.

Another question is about 'ret'.
http://llvm.org/docs/LangRef.html#i_ret gives the syntax:
   ret <type> <value>       ; Return a value from a non-void
function
   ret void                 ; Return from void function
In the case when the return type is not void, it returns
a single value. But if I am looking into the code,
the Verifier also allows 'multi returned values' if the return
type is of structure or array, while there is not interface
in 'ReturnInst' to create a multi-value 'ret'. Is it only for
the ll code that was generated by an old version LLVM
which had still supported 'multi-return'.

The comments in 'Verifier' say this 'multi-return' verification
feature may be removed from LLVM 3.0. So If I am generating
'ret' with multi values, will that be a verification error
when LLVM 3.0 releases?
>
> Nick
>


-- 
Jianzhou

On Sat, Mar 6, 2010 at 2:14 PM, Chris Lattner <clattner at apple.com>
wrote:
>
> On Mar 6, 2010, at 9:13 AM, Jianzhou Zhao wrote:
>
>> Hi llvm,
>>
>> 1) The lib/VMCore/Verifier.cpp in 2.7 implements Verifier::VerifyType,
>> which is empty in 2.6. I noticed that it does not check all types,
>> for example, UnionTyID, OpaqueTyID, LabelTyID, MetadataTyID
>> and etc are ignored in the 'default' branch. Does it mean we
dont
>> need to check them?
>
> They are leaf types (just like integer type), there is nothing to check.
>
>> Another question is: How much does Verifier.cpp check statically?
>> Can I take it as a type checker for SSA? Is there any static
>> semantics that has not been checked yet?
>
> The verifier is best effort, it does not guarantee correctness.
Can we take the verifier as a reference to generate correct SSA?
I had some confusions when I was reading the RefManual
on the LLVM website, so I looked into the source code of
Verifier to see how well-formedness is checked in practice.

For example,
1) Can I have a block that does not start with a label?
Verifier checks that a block must end with a terminator
instruction. If the block without a label is not the entry block
in a function, could that be jumped into? or is it still a valid block?
since the syntax allows the label to be optional.

2) Verifier checks a block must contain only one terminator
insn which must be the last insn, and phi insns must be
in the beginning of the block as a group. If this is the right grammar,
could we not change the syntax of blocks as..?
  phi* i* t* where
    phi is a Phi node, i is an insn except Phi and terminator,
    and t is a terminator node.
So we dont need to check this at runtime.
This is same to ask if the verifier is a module that we have to run.

Thanks.
>
>> 2) visitFreeInst has been removed from lib/ExecutionEngine/Interpreter
in 2.7
>> Will this have any back-compatible problem when interpreting any
>> *.bc from 2.6?
>
> The .bc reader will eliminate freeinst from the ir when reading an old
file.
>
> -chris


-- 
Jianzhou