Displaying 20 results from an estimated 31 matches for "formedness".
2010 Nov 28
3
[LLVMdev] RFC: Exception Handling Proposal II
...ue of %x1
>
> We expect the value printed to be 964, but if we don't allow %x1 to be accessible then we get garbage or an assert...
What do you mean by "otherwise valid"? Just that we can prove that %x1 has been computed by the time a throw can occur? We really want SSA well-formedness to be a simple structural condition; having to examine instruction-specific semantics to compute dominance would make it absurdly expensive to compute and keep valid. For example, if any instruction were valid to reference up to the first throwing instruction, then re-ordering the loads in the fo...
2013 Apr 03
3
[LLVMdev] Type-based analysis for LLVM IR
...ted in type-based verification of LLVM IR in the areas of
certified compilation and software verification. It seems to me that the
LLVM IR type system is rather informal in the sense that there is no paper
with a proper formalization of the type rules, and for example, a proof of
soundness for well-formedness of the code.
I would like to know if you are aware of any work in this direction for
LLVM IR so that I can compare with my own implementation.
Moreover, it would be valuable to get some feedback on suitable type-based
analysis that the LLVM community would like to have in the infrastructure.
Regar...
2010 Nov 28
0
[LLVMdev] RFC: Exception Handling Proposal II
...n() {
int x = 0;
try {
x = 37 + 927;
foo();
} catch (...) {
std::cout << x << '\n';
}
}
Any solution that violates this isn't a solution.
-bw
> Just that we can prove that %x1 has been computed by the time a throw can occur? We really want SSA well-formedness to be a simple structural condition; having to examine instruction-specific semantics to compute dominance would make it absurdly expensive to compute and keep valid. For example, if any instruction were valid to reference up to the first throwing instruction, then re-ordering the loads in the fo...
2001 Jun 11
0
Metadata Schema
...k wrote:
> There's no real way to parse an xml document on the fly, while
> maintaining it's well-formed-ness. We'd have to make each bit a
> standalone document. That doesn't make a whole lot of sense, and
> probably increases the overhead too.
It's true that well-formedness was one of the big advertised points of
the original xml spec, but I'm not sure it's worked out that way so much
in practice. Very few parser implementations are actually 'validating'
and a great deal of the error detect well-formedness provides depends on
the DTD design, where...
2004 Mar 27
1
[LLVMdev] verification
What are the different properties( well formedness of the intermediate code,
or other),if any that are verified by the verification phase in the LLVM.
2013 Apr 03
0
[LLVMdev] Type-based analysis for LLVM IR
...yping rules to perform verification, or
do you mean something else?
> verification. It seems to me that the LLVM IR type system is rather
> informal in the sense that there is no paper with a proper
> formalization of the type rules, and for example, a proof of soundness
> for well-formedness of the code.
Another important feature of the LLVM type system is that it is not a
"safe" type system. It is possible to do all sorts of type unsafe
things, such as casting integers to pointers and dereferencing them.
One of the standard LLVM transforms (load widening) will generate...
2011 Mar 10
0
[LLVMdev] Alternative to Adding New Intrinsics for Code-Generation?
...0, i32 0, i32 0)
> }
>
> Which generates this error in the verifying stage:
>
> Referencing function in another module!
> %value = call i32 @_function(i32 0, i32 0, i32 0)
That's asserting that @Test and @_function are in different llvm::Modules. That's a memory well-formedness constraints, not an IR constraint. That should honestly be getting checked for intrinsic functions, too.
John.
2019 Sep 10
2
Google’s TensorFlow team would like to contribute MLIR to the LLVM Foundation
On Tue, Sep 10, 2019 at 1:40 PM David Greene via llvm-dev <
llvm-dev at lists.llvm.org> wrote:
> Renato Golin via llvm-dev <llvm-dev at lists.llvm.org> writes:
>
> > But perhaps more importantly, as Hal states clearly, is the need for
> > an official specification, similar to the one for LLVM IR, as well as
> > a formal document with the expected semantics into
2011 Mar 10
2
[LLVMdev] Alternative to Adding New Intrinsics for Code-Generation?
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html;charset=ISO-8859-1" http-equiv="Content-Type">
</head>
<body bgcolor="#ffffff" text="#000000">
John McCall wrote:
<blockquote cite="mid:FAB334D8-72D0-40FB-B133-A9430870B701@apple.com"
2010 Nov 28
0
[LLVMdev] RFC: Exception Handling Proposal II
On Nov 27, 2010, at 4:57 PM, John McCall wrote:
> On Nov 25, 2010, at 3:03 AM, Duncan Sands wrote:
>> I'm pointing out that if the invoke instruction
>> is removed and catch information is attached to entire basic blocks, then if no
>> care is taken then it is perfectly possible to use %x before it is defined as
>> explained in my previous email, blowing up the
2007 Apr 21
0
Issues with Functional Tests
...using to display
the flash.
(2) One of the things I''d most like to test is simply whether the resulting
page is well-formed XHTML, to check if I''ve missed out any balancing tags in
my RHTML templates. Ideally I''d like "assert_result :success" to check for
well-formedness, or to have a separate assert_well_formed.
What would be the best way to achieve this? Does
assert_select "html"
by itself enforce that the entire document is well-formed?
(3) When using submit_tag, there doesn''t seem to be a simple way to do
:confirm => "Are you sur...
2010 Mar 06
0
[LLVMdev] Changes between 2.6 and 2.7: SSA Verifier and visitFreeInst
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
2019 Sep 11
5
Google’s TensorFlow team would like to contribute MLIR to the LLVM Foundation
...it is like if
you would split LangRef into:
- the definition of what is SSA, Module, Function, Block, terminator, phi
nodes. In particular that would be most of: Abstract
<https://llvm.org/docs/LangRef.html#abstract>, Introduction
<https://llvm.org/docs/LangRef.html#introduction>, Well-Formedness
<https://llvm.org/docs/LangRef.html#well-formedness>, Identifiers
<https://llvm.org/docs/LangRef.html#identifiers>, High Level Structure
<https://llvm.org/docs/LangRef.html#high-level-structure>, Module Structure
<https://llvm.org/docs/LangRef.html#module-structure>, and par...
2010 Mar 09
1
[LLVMdev] Changes between 2.6 and 2.7: SSA Verifier and visitFreeInst
...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 sy...
2010 Nov 28
5
[LLVMdev] RFC: Exception Handling Proposal II
On Nov 25, 2010, at 3:03 AM, Duncan Sands wrote:
> I'm pointing out that if the invoke instruction
> is removed and catch information is attached to entire basic blocks, then if no
> care is taken then it is perfectly possible to use %x before it is defined as
> explained in my previous email, blowing up the entire LLVM system. Clearly the
> solution is to not allow this by not
2010 Nov 28
6
[LLVMdev] RFC: Exception Handling Proposal II
...#include <iostream>
> extern void foo();
> int main() {
> int x = 0;
> try {
> x = 37 + 927;
> foo();
> } catch (...) {
> std::cout << x << '\n';
> }
> }
>
> Any solution that violates this isn't a solution.
These well-formedness constraints on IR are not constraints on actual user code, they're constraints on frontends and transforms. Frontends have to translate actual user code into well-formed IR, and transforms have to preserve well-formedness.
In your example, a C++ frontend is going to generate this code with %x...
2008 Apr 24
0
[LLVMdev] templates vs code to generate IR
Hi Terence,
The reason I remarked, actually, is that for LLVM in particular the C+
+ API offers more safety, and emitting .ll generally requires at least
partially reimplementing the IR object model. I think this is a topic
in the FAQ. But both are perfectly valid approaches!
- Gordon
On Apr 23, 2008, at 14:04, Terence Parr <parrt at cs.usfca.edu> wrote:
> Gordon reminded me that
2008 Apr 23
2
[LLVMdev] templates vs code to generate IR
Gordon reminded me that most people seem to generate code using code,
whereas it has become natural for me to use templates to generate
code. Let me include an example from an article I'm working on (Java
centric). The same argument goes for LLVM IR templates versus using
the C++ interface. Generating LLVM IR for me is super simple. Here
are a few of my templates for generating IR
2010 Mar 06
4
[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
2011 Jul 29
0
HTML sanitization
...mple.com/">` the same way regardless of whether it
was generated from `` or just included
literally in the source; the disadvantages are that it may be even slower
than the other alternatives (making an additional pass over markup whose
well-formedness and safety is guaranteed by construction), it could be a
little more bug-prone ("Where did all of my `<ol>`s go? Oh, I left `ol` out
of the whitelist."), and it doesn't facilitate intermediate processing in
any way.
[yamemex]: https://github.com/kragen/yamemex/tree/...