<rwmjones>
but yes qemu can now emulate aarch64 userspace fine, and runs all the ocaml binaries I threw at it
<rwmjones>
it doesn't emulate the full aarch64 system though
<mrvn>
oh? Iphone5 or is there some other hardware?
<rwmjones>
it doesn't emulate the full system
<rwmjones>
oh you mean my hardware? it's under NDA
<rwmjones>
it's not an iphone :-)
<whitequark>
actually, having iphone support in ocaml would be interesting to me
<rwmjones>
AFAIK no one has liberated the iphone 5S
<mrvn>
ocaml binaries should run on android
<rwmjones>
so you couldn't just run a general purpose OS on it .. be interesting if it was possible
<whitequark>
rwmjones: don't care, I want to make an app
<whitequark>
running GPOS on iPhone is somewhat pointless
<adrien>
rwmjones: wondering: when is the hardware you have supposed to go out?
<mrvn>
rwmjones: some years ago linux support for hardware lagged years behind. Now we have full linux support for aarch64 and there isn't even hardware out there.
<adrien>
been using freescale's BSP at work for imx6; I wouldn't say that...
<adrien>
(and freescale is among the most up-to-date and upstream ones)
<rwmjones>
it's under NDA, I can't answer any questions about it ..
<adrien>
not even when the nda is off? damn :P
<mrvn>
adrien: imx6 ia arm, nor aarch64
<adrien>
yes, and it's already out and it's been some time, but the BSP are quite behind imho
nikki93 has quit [Remote host closed the connection]
nikki93 has joined #ocaml
ygrek_ has quit [Ping timeout: 252 seconds]
araujo has joined #ocaml
nikki93 has quit [Remote host closed the connection]
nikki93 has joined #ocaml
BitPuffin has quit [Ping timeout: 240 seconds]
boogie has quit [Remote host closed the connection]
tlockney_away is now known as tlockney
SethTisue has joined #ocaml
rgrinberg has joined #ocaml
<jpdeplaix>
whitequark: is it normal that LLVM does an optimization pass that change the semantic ?
johnnydiabetic has joined #ocaml
<jpdeplaix>
I've a non-terminating recursive function which does a side-effect and it replace it by a « unreachable + llvm.trap »
<whitequark>
jpdeplaix: that means you have UB there
<whitequark>
i.e. it is normal if LLVM can prove that your function dynamically invokes UB on all codepaths
<Anarchos>
where to download camlp4 ?
<whitequark>
Anarchos: github.com/ocaml/camlp4, but if you just need to install it, opam install camlp4
<mrvn>
I think that is realy realy realy realy stupid. If it can proof UB then it should give an error.
<whitequark>
mrvn: that is not how C works
<mrvn>
not silently mangle the code.
<whitequark>
mrvn: I mean, I agree, but if LLVM wants to support a C compiler, it must work like that.
<mrvn>
no
<mrvn>
nothing says that a single UB instruction shall optimize away whole functions
<whitequark>
well
<whitequark>
UB is the language's way of saying "this is never dynamically reachable"
<whitequark>
so if a function invokes UB, it is never dynamically reachable
<mrvn>
how is undefined behaviour dead code?
<whitequark>
that's how C works :)
<whitequark>
let me explain with an example
<whitequark>
let's begin with a benign one. "if (p1 != p2) { memcpy(p2, p1); }"
<whitequark>
errr
<mrvn>
It's like eliminating { printf("This should never happen\n"); assert(false); } because the assert can never be true.
<whitequark>
"if (p1 != p2) { memmove(p2, p1); }"
<whitequark>
in this case, since the compiler can prove that p1 and p2 do not alias, it can use a more efficient version of memmove, namely memcpy.
maattdd has quit [Ping timeout: 240 seconds]
<whitequark>
(I am simplifying it)
WraithM has joined #ocaml
<whitequark>
then you have a case like this: "p->x = 1; p->y = 2; (do something else with p)"
<whitequark>
as the first statement would invoke UB if p = NULL, after it executes, the compiler can safely assume that p is never NULL
<whitequark>
or it works similarly for e.g. division by zero
<whitequark>
the idea behind UB is that it's a way to guide the automated theorem prover inside the optimizer by saying to it "this case never happens, but you're too dumb to discover this on your own"
<mrvn>
whitequark: the problem is that it eliminates good code because somewhere inbetween there is minor dirty bit.
<mrvn>
without warning or error
<whitequark>
the problem is basically that you can say "here you are, an axiom: False = True"
<mrvn>
If it can proof that the code is bad it should simply give an error
<whitequark>
it's not "bad"
<whitequark>
there's no concept of "bad" code that exists in C
<Anarchos>
whitequark i can't use opam.
<mrvn>
whitequark: there is undefined behaviour
<whitequark>
if the compiler can prove that (statement|branch|loop|function) invoke UB, it considers them unreachable
<whitequark>
because that is what the standard requires
<mrvn>
but UB is NOT unreachable. It is just undefined.
<whitequark>
no, it IS unreachable, or must be treated like that according to the standard
<mrvn>
and the standard does not require that.
<ggole>
The standard doesn't require anything at all from UB
<ggole>
It can crash the compiler, etc
<ggole>
(And often used to, back in the day.)
<whitequark>
ok, "must" is not the right world here, let me rephrase
<mrvn>
And it is certainly not the expectation of the programmer that a signed integer overflow will simply remove whole chunks of code instead of simply overflowing in the cpu register and continue.
<whitequark>
some uses of UB are legitimate (i.e. when UB is never dynamically invoked), and the compiler must take advantage of them in order to be competitive with other compilers, which do.
<mrvn>
whitequark: "Must" is totaly the wrong word. "can" is the right word. That doesn't make it smart.
<whitequark>
a compiler which would do the most conservative thing that can possibly happen if UB is invoked certainly conforms to the standard
<whitequark>
it also won't be widely used
<mrvn>
whitequark: if the UB is never invoked then it is dead code.
<whitequark>
mrvn: the problem is that you can't, in general, prove that UB never happens, it's turing-complete
<mrvn>
and dead code can be removed. But just being UB doesn't make code dead.
<ggole>
It'd be interesting to know what the actual improvement is
<whitequark>
ggole: apparently, the undefinedness of signed overflow improves some tight loops quite a bit
<whitequark>
even if it wasn't originally designed for that, but rather for 1's complement machines
<ggole>
I'd guess that most of it is totally useless.
<ggole>
With some obvious exceptions, eg, array bounds
<whitequark>
afaik, it's due to the fact that it allows vectorization, because the optimized code doesn't have to check for overflow to remain equivalent to the original
<whitequark>
quite a bit of it stems from the type system, which is too incoherent to express anything interesting at all
<mrvn>
ggole: signed overflow is undefined because the result differs on 1s and 2s complements. And now the compiler says: Hmm, if we overflow here the behaviour is undefined and I can do whatever I like. So lets assume we don't overflow since if we do the code is still correct.
<whitequark>
TBAA is a joke
<whitequark>
mrvn: see above on why the undefinedness of signed overflow is exploited in practice
<mrvn>
example: signed char i = 0; char buf[256]; do { buf[i++] = 0; } while (c != 0);
SethTisue has quit [Ping timeout: 240 seconds]
<ggole>
The right way to do it IMHO is to have a defined language with explicit unsafe operations that admit UB for performance hackery only where needed
<mrvn>
You would think that zeroes buf and stops. Instead if keeps going for i=256, i=257, i=INT_MAX, ...
<ggole>
Then you can find your tight loop and specify that index arithmetic can assume no overflow, and everything else can be sane.
<whitequark>
mrvn: it doesn't keep going
SethTisue has joined #ocaml
<mrvn>
whitequark: update your gcc
<whitequark>
it does whatever the hell your compiler pleases. for example, traps.
<gasche>
rwmjones: making a github PR is in no way mandatory to get a patch taken into account
<whitequark>
lol, as if gcc is the only C compiler that exists
<gasche>
(we don't "depend" on it, it's just a convenience that some people requested)
<gasche>
I saw your patch, but I'll check with someone that knows better about backends before upstreaming it
<gasche>
it looks simple enough to go quickly, though
<mrvn>
whitequark: I know it can do whatever it wants. In the case of gcc it puts the char into a register and considers it an int.
<whitequark>
mrvn: your statement does not make sense. you cannot reason like that about code with UB.
<gasche>
(the argument-handling one for example would require a more careful review, for which we don't have much time before the release this summer)
<whitequark>
you can say that "on gcc version X.Y.Z with flags (list of flags) and architecture A it does the following"
<whitequark>
but no less than that.
<whitequark>
mrvn: LLVM optimizes this to "int main() { return 0; }"
<mrvn>
whitequark: All i showed is that gcc ignores the undefined overflow and assumes that never happens in its optimizer phase.
<mrvn>
whitequark: And that is wrong.
* whitequark
shrugs
<mrvn>
whitequark: LLVM took a code with UB that should crash and suddenly produces a binary that simply skips the code.
<whitequark>
it's wrong to think that UB "should" crash.
<mrvn>
the compiler noticed the UB, can proof it is UB. It should not ignore that. UB in code is a bug.
<whitequark>
if you want UB to always crash, add some instrumentation to your C compiler and use it. -fsanitize=undefined will take you a long way.
<whitequark>
your approach does not in general make more sense than what happens in general.
<whitequark>
for example, it is extremely hard to make a sensible error message explaining the specific conditions where UB happens
<mrvn>
my approach lets the programmer know that he wrote garbage.
<whitequark>
"hey, somewhere in these 5MLOC of code there is an UB. fuck this, I'm out"
<whitequark>
it's useless
<mrvn>
better than having the nuclear powerplant fail to shut down when an earthquake hits.
<whitequark>
take a look at what static analyzers do. in fact, they *ignore* certain known cases of UB, if they're too complex to sensibly explain, because if they don't, the users get annoyed by false positives and *stop using the analyzer whatsoever*
<whitequark>
ha, don't program the powerplant in C. that's way simpler than trying to fix C while remaining compliant.
<ggole>
Lots of embedded stuff is written in C :/
<ggole>
Car systems, etc
<whitequark>
or, program the powerplant in something else and then extract the code to C, that's basically how it works in automotive field (for example)
<mrvn>
if they are false positives then the compiler can't optimize them away. So that case is not what we are talking about.
<ggole>
(They usually compile without optimisations though.)
<whitequark>
mrvn: "this function always invokes UB" can easily be a false positive, if it's not main.
<mrvn>
whitequark: if the logic has false positives then it can't optimize that away. That would give wrong results for correct input.
<whitequark>
ggole: there's the MISRA set of standards, which basically restrict you to a tiny subset of C and force you to prove your logic correct
<mrvn>
whitequark: so choose: 1) the compiler is buggy, 2) it doesn't have false positives
<ggole>
MISRA has nothing to do with correctness, it's just a coding standard
<ggole>
No recursion, etc
jpeeters has left #ocaml [#ocaml]
<whitequark>
ggole: it eliminates a great deal of possible UB sources
<whitequark>
mrvn: that *may* give wrong results for correct input
<whitequark>
and the job of the programmer is to ensure that it does not.
<whitequark>
again, LLVM (or gcc or...) implements C exactly as the standard intends it to be implemented. it's broken by design, not broken in the compiler
<whitequark>
you can complain to the people who write C, or to the people who use compilers with optimizations, or to the people who define C, but the compiler works as it should
<ggole>
And there's no way to tell that UB exists other than reading the source and understanding it all. Yay.
<mrvn>
whitequark: sorry, if the compiler falsly detects UB and optimizes that away that it is simply buggy. That is not what the standard says.
WraithM has quit [Ping timeout: 276 seconds]
<whitequark>
what?
<whitequark>
I never talked about "falsly detecting UB"
<mrvn>
whitequark: you did. you said it has false positives.
<whitequark>
by "false positives" I mean cases where the static analysis shows that UB may happen, but dynamically it never does
<whitequark>
because of an invariant that the analyzer is not aware of
<mrvn>
whitequark: and those you can't optimize away. You can only optimize away cases where is always hase UB.
<whitequark>
if UB merely "may" happen, the compiler can't just optimize it away
<whitequark>
correct
<mrvn>
whitequark: bingo. that's what I have been saying all along
<whitequark>
but consider the scope of the analysis
<whitequark>
surely, if the compiler can prove that a program *always* invokes UB, it could display an error
<whitequark>
but how do you actually check for that for any non-trivial case?
<mrvn>
whitequark: All I'm complaining about are the "is always undefined behaviour" cases.
<flux>
don't they do that already, in the form of warnings, for some cases?
<whitequark>
you can't do whole-program analysis for a program of any interesting size
<whitequark>
not really, those are basically syntactical
<whitequark>
like it pattern-matches *((ptr*)0)=...
<whitequark>
because it's a common pattern to write (sigh)
<mrvn>
whitequark: irelevant. both gcc (>= 4.8) and llvm do some analysis and optimized "always UB" cases away.
<whitequark>
mrvn: not irrelevant.
<whitequark>
if you only work *at a function level*, which optimizers in general do, you can't say anything about the *whole program*
<mrvn>
whitequark: I'm only talking about the cases it does find. So the fact that it doesn't and can't find all cases is irelevant.
<whitequark>
except for some really restricted cases where you have a non-conditional codepath from main()
<ggole>
It's not necessarily the case that they go looking for UB and then activate some special program-destroying code if found
<whitequark>
ggole: that's actually what happens
<ggole>
Often these things are assumptions that are baked into passes
<whitequark>
if a compiler can prove that a *function* always invokes UB, it optimizes it to "unreachable"
<mrvn>
ggole: and that is a problem
<whitequark>
(among other things)
<ggole>
That's a subset of the UB that you would want reported, though
<whitequark>
ggole: nope
<mrvn>
whitequark: and that is simply wrong (although not against the standard). UB != dead code.
<whitequark>
if the function is never called, it's perfectly OK
<ggole>
What does that have to do with error reporting?
<whitequark>
ggole: saying, say, "function f always invokes UB" is easy
<mrvn>
"people don't want to get warnings about undefined behavior in dead code" problem
<whitequark>
but in practice you will have much more complex preconditions, say, "function f when invoked with arguments A and B always invokes UB" (and it can say that because it inlined f)
<mrvn>
imho people are wrong there#
<ggole>
Right, and compilers should do that. But there are other cases that you would want reported, as I've already said.
<whitequark>
and it very quickly becomes intractable
<flux>
I would love to be able to optionally enable warnings that tell me that there is a way this code is UB.
<flux>
cool, gotta try that next time I code C or C++ :)
<ggole>
It's intractable, so let's have the programmer do it. That's C in a nutshell.
<whitequark>
ggole: exactly
<mrvn>
flux: the "may be UB" is much harder
<whitequark>
mrvn: flux: clang-analyzer shows the entire codepath leading to the issue
<whitequark>
it is really good in practice
<ggole>
-fsanitize is a dynamic checker, right?
<flux>
mrvn, yes, of course I would like to non-optionally see warnings of cases where it's always ub, regardless how it's called, even possibly outside the compiler's view
<flux>
let's say you have function { if (ptr) return 0; value = *ptr; return value; } I would certainly like the compiler to complain about UB, if it actually does optimize that to plain return 0 :). (even if I don't call it)
<whitequark>
ggole: yes
<ggole>
That's probably the most practical way forward.
<flux>
mrvn, because if ptr is null, it dereferences it
<whitequark>
mrvn: if (ptr) check fails, therefore ptr is null
<whitequark>
then it does *ptr
<mrvn>
ah, nm.
<mrvn>
I would like a "Warning: dereferencing NULL" there
<whitequark>
mrvn: then build all your code with clang-analyzer
<whitequark>
problem solved
<whitequark>
hm, let me build ocaml with it
<mrvn>
"Ultimately, undefined behavior is valuable to the optimizer because it is saying "this operation is invalid - you can assume it never happens". In a case like "*P" this gives the optimizer the ability to reason that P cannot be NULL. In a case like "*NULL" (say, after some constant propagation and inlining), this allows the optimizer to know that the code must not be reachable."
<mrvn>
And that is the problem with LLVM. UB != dead code.
<whitequark>
mrvn: s,LLVM,all major compilers,.
<flux>
mrvn, would you be not be happy to at least see: "Warning: dead code" there?
<mrvn>
It assumes the input is 100% correct while we all know it hardly ever is.
<whitequark>
again, go complain to those who write and use C, not compiler authors
<NoNNaN>
and what about "undefined" code, something like for random seed generation ?
<mrvn>
whitequark: that is not a problem of C. That assumption that UB code must be unreachable is purely llvm.
<whitequark>
mrvn: lolwhat?
<whitequark>
the assumption is shared by all major compilers. gcc, icc, armcc, you name it
<whitequark>
if clang wants to be competitive, it must share it too
<NoNNaN>
a few years ago debian fixed a random generation bug in ssh
<whitequark>
NoNNaN: that code is broken, don't write it
<whitequark>
you cannot assume that the contents of a freshly allocated buffer would be random
<whitequark>
in fact, it's usually zeroes, for security reasons
<mrvn>
whitequark: eat shit, a million flies can't be wrong. :)
<whitequark>
mrvn: that's how markets work, yes
<flux>
mrvn, so what they should do instead? somehow implement UB behavior, which really doesn't make sense, and be slower because of it?
<whitequark>
flux is correct, if LLVM would be perceived as "slower" and "inferior" it will simply not be used.
<flux>
"our optimizer says this makes no sense, but let's do it anyway"
<NoNNaN>
i am not a fan of UB, but it may have some legitimate use case
<mrvn>
flux: compile the maybe UB code and flag the branches as unlikely.
<whitequark>
mrvn: that inhibits downstream optimizations, e.g. the vectorization case I have outlined earlier
<mrvn>
whitequark: so? At least it doesn't eliminate code that is actualy going to be reached.
<whitequark>
mrvn: the generated code is slower
<whitequark>
people go on slashdot and say that LLVM is shit
<whitequark>
etc
<whitequark>
you are free to complain that people are wrong and stupid, of course, and you may even be right, but that won't change anything
<whitequark>
to paraphrase, "every C compiler evolves until it aggressively optimizes out UB, and those who don't are replaced by those who do"
<flux>
forking your own clang will :). actually you need to for llvm as well, because the concept of 'poison value' is supported there as well.
<NoNNaN>
these people probably already written a competetive compiler toolkit
tlockney is now known as tlockney_away
<whitequark>
NoNNaN: well, there's always some other one. gcc, for example
<whitequark>
which does the exact same thing with UB as clang, sometimes even more aggressively
thomasga has quit [Quit: Leaving.]
<mrvn>
and look how much surprise that produced when gcc-4.8 did it.
<flux>
it didn't suprise folks that program with sane languages ;-)
<mrvn>
.oO(like ocaml)
<adrien>
I'm definitely surprised when I see something optimized in OCaml :P
<NoNNaN>
the language has a standard, and also a formal semantics model (k-framework.org subproject), and also has dark corner cases...
maattdd has joined #ocaml
thomasga has joined #ocaml
<rwmjones>
gasche: thanks .. it is the aarch64 patch I'm most concerned about
maattdd has quit [Ping timeout: 252 seconds]
maattdd has joined #ocaml
axiles has quit [Remote host closed the connection]
BitPuffin has joined #ocaml
ygrek_ has joined #ocaml
Eyyub has quit [Read error: No route to host]
BitPuffin has quit [Ping timeout: 240 seconds]
ollehar1 has joined #ocaml
ollehar1 has quit [Client Quit]
WraithM has joined #ocaml
<whitequark>
hmm, ran clang-analyzer on ocaml. scan-build: 25 bugs found.
<whitequark>
almost all of them are in yacc
<whitequark>
hm, why does ocaml even *have* a C yacc runtime? O_o
ollehar has quit [Ping timeout: 240 seconds]
<gasche>
hopefully we'll use Menhir instead medium-term
<whitequark>
gasche: no, I mean, what is the point?
<whitequark>
where does it use yacc?
<gasche>
the OCaml parser uses ocamlyacc
<whitequark>
oh, it's not the usual yacc thingy, it's the OCaml-specific one
<gasche>
but it outputs C code, so the runtime is in C indeed
<whitequark>
caml_insert_global_root can apparently dereference NULL
<whitequark>
gasche: hm, how to build OCaml runtime with assertions? is there some flag?
<whitequark>
--with-debug-runtime, nevermind
<whitequark>
"Dereference of null pointer" with path length 48 ಠ_ಠ
<whitequark>
mrvn: see, this is why static analysis sucks
<def`>
yay hopefully switching to menhir soon
<whitequark>
def`: 4.03? :)
<def`>
likely
<jpdeplaix>
whitequark: mmmh in fact after having reduced the test-case it seems that it only occurs when all the functions have the fastcc call convention
arj has quit [Remote host closed the connection]
<whitequark>
jpdeplaix: oh, verify that the call site and the function itself have the identical calling convention
<whitequark>
if it's not the case, LLVM just turns the call site into a trap
<Drup>
( whitequark : funnily, I would say that's why static analysis is awesome : it just found a corner case that could potentially happen but that no sane human would fine and that would be a nightmare to debug)
<whitequark>
Drup: I understand your point, but now look at it from another angle
<whitequark>
most likely, the potential benefit from fixing this is far lower than the required cost
<Drup>
sure
<whitequark>
it's a moot point for ocaml, which has less than a dozen bugs found by clang-analyzer, but if you imagine a big commercial codebase... you'll realize why the vendors of static analyzers have quite a hard time selling them
<Drup>
that's why it's a tool, not a default verification.
BitPuffin has joined #ocaml
<Drup>
oh, right
<Drup>
I get your point
<Drup>
you're just saying that it should triage issues.
<def`>
a codebase being too bad to be easy to correct is not really a point against static analysis
<whitequark>
def`: it's a point against commercial application of static analysis
<whitequark>
or to phrase it another way, "here is why the vendor of $IMPORTANT_THING is not going to use static analysis"
<Drup>
"because their software is so shitty that the static analyzer goes crazy"
<def`>
whitequark: 'we are doing it so wrong that we should better close our eyes'
<whitequark>
Drup: def`: exactly
<Drup>
whitequark: no but, in practice, you do have a point about triaging warning reported by the static analyser
<adrien>
nah
<Drup>
but it's not as easy has it sounds.
<adrien>
what you mainly want to do is close the eyes of customers :P
<Drup>
as*
WraithM has quit [Ping timeout: 255 seconds]
<def`>
so selling true(1) as a static analyser is a quick way to get rich :)
<whitequark>
def`: you'd have to justify its cost somehow
ggole has quit []
<whitequark>
but, uhhh, actually, I'm sure there are a few products which are marginally better than true(1) and sell well...
<Drup>
whitequark: put it on the bug tracker, def` will be very happy to have a new argument for killing yacc in profit of menhir
<whitequark>
Drup: hmm, good idea
<whitequark>
although I first need to figure out why it still thinks that Assert() is a no-op
<whitequark>
despite passing --with-debug-runtime
<Drup>
"Result of operation is garbage or undefinedotherlibs /graph /color.c" <- wut ?
<whitequark>
Drup: what's unclear?
<Drup>
the content
<whitequark>
why the shift is undefined?
Eyyub has joined #ocaml
<Drup>
yes
<Drup>
(I'm not very good in C, be gentle)
<jpdeplaix>
whitequark: OH ! You're right. For direct calls it's called with the good cc, but for the indirect calls (extracted from the closure) it doesn't use the good cc
<whitequark>
Drup: ... honestly, I have no idea either
<whitequark>
let me look at the standard.
<Drup>
(I must say the output is nice)
<whitequark>
in principle, shifts are undefined if you shift the sign bit out of its place, and also if you shift too far
<whitequark>
but I don't see how either of those will *always* be true on this path
<whitequark>
oh, shifting the sign bit out is IDB, not UB
<Drup>
idb ?
<whitequark>
so UB would only happen if caml_gr_red_r < 0 or -//- > sizeof((i << 8) + i)*8
<whitequark>
implementation-defined behavior
SethTisue has quit [Quit: SethTisue]
<Drup>
ok
<whitequark>
"do whatever you want, but consistently, and document it"
<whitequark>
there's also unspecified, "do whatever you want, but consistently, and don't document it"
ontologiae has joined #ocaml
<jpdeplaix>
whitequark: thanks. It works now ! :)
<whitequark>
there appear to be race conditions in the parallel build of OCaml, exacerbated by the slowness of clang-analyzer...