--- Log opened Wed May 15 00:00:13 2019
02:58 -!- afk11 [~afk11@unaffiliated/afk11] has quit [Ping timeout: 255 seconds]
03:08 < real_or_random> yeah the problem is that it does not support memcpy and memcmp ^^
03:13 < gmaxwell> real_or_random: here ya go https://0bin.net/paste/sfj0FP+tFUcMKWnd#sUG0ekMdOMUp+SEJRoK1-0OnCyXUyCrMs9shJcmlC0F
03:15 < real_or_random> ok yes... I had the same idea but I'm not convinced that this works. I mean if it works, why don't they include these implementations? hm but we should try it at least
03:19 < gmaxwell> I would just assume because it doesn't have other system functions that it can't just use system headers. And if someone is going to implement them, it might as well be you.  There isn't anything special about the behavior of memcpy or memcmp in C.
03:23 < real_or_random> (depends on your C version, I think in C89 it was not possible to implement memcpy because reading padding bytes gave you instant UB)
03:24 < real_or_random> but maybe there's something special about memcpy in compcert's subset of C.. whatever I'll try it
03:28 < real_or_random> https://github.com/AbsInt/CompCert/issues/28#issuecomment-78102445 related
03:35 < gmaxwell> I wouldn't be shocked if we never copy a struct with memcpy, we should be just using assignment for that. so even if thats the issue perhaps we'll mostly be okay. :)
03:35 < gmaxwell> tests might be sloppier though
03:39 < real_or_random> hehe your memcpy implementation has the wrong return type
03:40 < real_or_random> it actually returns the dst pointer (for whatever reason)
03:43 < gmaxwell> oh indeed, lol just saw void in the prottype ..
04:56 < real_or_random> gmaxwell: okay when I give it implementations of memcpy, memcmp and memset, then it does not die quickly for tests and tests_exhaustive
04:56 < real_or_random> but then it runs out of memory on my machine^^
05:00 < gmaxwell> lol
05:07 < real_or_random> but yep. until that point there's no UB :P
06:23 -!- sipa [~pw@gateway/tor-sasl/sipa1024] has quit [Remote host closed the connection]
06:23 -!- sipa [~pw@gateway/tor-sasl/sipa1024] has joined #secp256k1
08:25 -!- belcher [~belcher@unaffiliated/belcher] has quit [Quit: Leaving]
10:04 -!- roconnor [~roconnor@host-184-164-20-227.dyn.295.ca] has joined #secp256k1
10:06 < roconnor> I think you need to qualify that statement.  I'm skeptical that the compcert interpreter detects all forms of UB, and I would be moderately surprised if they detect signed integer overflow.  But maybe I'm wrong since I don't really know anything about the compcert interpreter.
10:09 < real_or_random> okay, so I don't know much either. what it does it interprets your (subset of) C code using real semantic reduction rules
10:10 < real_or_random> this should catch almost all UB in that particular execution trace
10:10 < real_or_random> of course, that does not mean there is no UB for other inputs, and it becomes interesting when it comes to non-determinism
10:11 < real_or_random> for example, they have a special mode that tries different execution orders in a single statement, because this is UB too if the result depends on it
10:14 < real_or_random> so I assume this catches signed overflow. (this interpreter is also terribly slow, which somehow supports my assumption)
10:15 < roconnor> I see.  I don't suppose you'd be willing to add a signed intereger overflow to the main test function.
10:16 < roconnor> (or even better, multiply two large unsigned short values together. *lol*
10:17 < real_or_random> :D yes
10:20 < real_or_random> btw, secp256k1 has a lot of multiplications of uint16_t's. assuming an implementation of C where int is 64 bits, this is pretty evil
10:20 < real_or_random> sorry, I meant uint32_t
10:23 < roconnor> Yes.
10:24 < roconnor> I can provide a patch to fix it, if people are actually interested.
10:25 < real_or_random> I don't think it's worth the hassle
10:26 < roconnor> FWIW, I write my code as follows to avoid the issue: https://github.com/ElementsProject/simplicity/blob/C/libsha256compression/sha256/compression.c#L30-L33
10:26 < real_or_random> but seriously, this is the really the part where I lost faith in C. I always thought: okay, all of this is not portable anyway but you can use those nice portable integer types. but just no, you can't... ^^
10:26 < real_or_random> yes, that's the easiest and probably most readable way to do it
10:27 < roconnor> based on my cursary glance, it has no runtime impact on a reasonable compiler.
10:27 < roconnor> But maybe libsecp256k1 is full of other portability issues, so maybe it isn't worth tackling.
10:27 < real_or_random> well if it had impact, then we probably had a bug now
10:29 < real_or_random> s/had a bug/would have a bug
10:32 < roconnor> If the comcert interpreter detects UB in the product of large unsigned short values, I will be very impressed.
10:33 < roconnor> I'll task it to detect UB in interior out of bounds access to multidimentional arrays next. (i.e. accessing foo[0][2] in a char foo[2][2] array).
12:39 < gmaxwell> real_or_random: you can do multiplications of uint32_ts fine where hardware where int is 64 bits.  You might be unhappy if 32-bit int multiplies are _slow_ but with the exception of cray smaller types have generally been well supported... and then there are the uint_fast32_t types...
12:41 < gmaxwell> roconnor: why would that impress you? gcc -fsanitize=undefined  detects when arithmetic overflows signed integers fairly (but not perfectly) reliably.
12:45 < roconnor> gmaxwell: the issue is that if UINT32_MAX is less than INT_MAX then if the product of two uint32_ts exceeds INT_MAX then the result is undefined behaviour.
12:47 < roconnor> "impressed" was probably the wrong word. "suprised" is perhaps better.  I would be suprised because CompCert's computation model, or whatever it is called, defines signed integer overflow.  I.e. Today's CompCert provably perserves the twos-complement overflow of signed integers.  So if their interpreter caught an error that isn't an error in their computaitonal model, that would suprise me.
12:47 < gmaxwell> ah, makes sense that you would be surprised there.
12:48 < gmaxwell> Wait, why would the product of two uint32s not fitting in int be UB?  the product of uint32s should be a uint32 not an int.
12:48 < real_or_random> integer promotions
12:49 < real_or_random> they're first converted to int (not unsigned int!)
12:50 < roconnor> C allows any type that fits in a signed int to be promoted to a signed int prior to (any?) operatation.  so if UINT32_MAX <= MAX_INT then the compiler is allowed to promote the uint32_ts to signed integers and perform the multiplication there and convert back.  But if the signed integer multiplicaiton overflows, then you get UB.
12:50 < real_or_random> it's not just allowed, it's required
12:52 < gmaxwell> oh indeed. I was focused on the size in your example, not the signedness.
12:53 < real_or_random> and compilers do exploit that in practice. that's super weird
12:53 < gmaxwell> real_or_random: yes but also they treat a large amount of UB as implementation defined.
12:53 < real_or_random> so the right way to multiply two variables a, b of unsigned integer type is not a*b but 1U*a*b
12:54 < gmaxwell> promotion rules generally suck (if you go through #bitcoin-dev history you can see me whining about people turning loop counters into unsigned types becuase it makes unfavorable interaction with promotion rules much more likely)
12:54 < real_or_random> then (1U*a) forces a to be converted to unsigned int
12:54 < roconnor> forced to be converted to the larger of the type of a and unsigned it.
12:55 < roconnor> *unsigned int.
12:55 < real_or_random> right
12:55 < real_or_random> the irony here is that all the uintX_t are supposed to be portable (and typically sold as portable)
12:56 < real_or_random> but the entire semantics of integer operations depends on the number of bits in an int, no matter if you use an int or not
12:58 < gmaxwell> real_or_random: so did you get the interperter running? or do I need to runn it on a machine with 256 or 512 GB ram?
12:59 < gmaxwell> roconnor: the thing I'm most interested in hearing from the interperter is code whos behavior depends on sequence point/argument order violations, which no other tool I've used will detect but the ccomp interp will.
13:00 < roconnor> for sure!
13:00 < real_or_random> lemme push a hacked branch, then you can run it
13:00 < roconnor> I mean, assuming it does that.
13:01 < roconnor> I was under the impression that compcert's C-subset might disallow more than one memory write per command.
13:01 < roconnor> or something like that.
13:02 < gmaxwell> roconnor: at least a number of years ago (when there wasn't any real prospect of getting libsecp256k1 to run in it :) ) it would do that.
13:02 < real_or_random> https://github.com/real-or-random/secp256k1/tree/compcert-hack
13:03 < real_or_random> it sets count=1, and the seed to all zeros (because we can't have fread() etc) in the tests, and adds the string functions
13:04 < real_or_random> then I ran it using "ccomp -interp src/tests.c -I. -DUSE_NUM_NONE -DUSE_FIELD_INV_BUILTIN -DUSE_SCALAR_INV_BUILTIN -DUSE_FIELD_10X26 -DUSE_SCALAR_8X32 -DVERIFY"
13:45 < gmaxwell> how do you keep it from picking up system headers that it can't handle?
13:50 < gmaxwell> it's blowing up for me because /usr/include/bits/floatn.h uses _Complex
14:15 < gmaxwell> real_or_random: got it going, took a lot of additional mods.  found some actual but inconsequential undefined behavior in -DVERIFY already
14:16 < real_or_random> oh didn't see. it worked for me without further mods and was running for quite a while
14:16 < gmaxwell> Stuck state: in function secp256k1_fe_sqr_inner, expression !(25U >> 38 == 0)
14:16 < gmaxwell> Stuck subexpression: 25U >> 38
14:16 < gmaxwell> real_or_random: weird, compcert 3.5?
14:17 < gmaxwell> real_or_random: I had to go and find all fprintf(stderr,  and turn them into printfs
14:17 < gmaxwell> and a number of other small things.
14:17 < real_or_random> yes 3.5
14:17 < real_or_random> maybe it never got to that point on my machine
14:18 < gmaxwell> I'm also running on ppc64, it might behave somewhat differently (compcert was supported on ppc for a long time before x86)
14:18 < gmaxwell> hm. this output is not the most informative!
14:19 < gmaxwell> https://0bin.net/paste/UG1E+QSUUUxW3QRR#WYOGFiAIVlssIhmRXYCgKwtZ859cU1OnuhBDECmn97f
14:19 < real_or_random> ah I think on ppc64 it has a 128bit integer extension even
14:20 < real_or_random> yes you can run it with -dc
14:20 < real_or_random> or -cd ?
14:21 < real_or_random> then it outputs the .c file after some compcert-specific preprocessing. not sure if this is clearer
14:21 < real_or_random> the error messages are not very detailed, yes
14:34 < gmaxwell> -trace is ... very detailed
14:36 < real_or_random> could you figure out the <loc>?
14:36 < roconnor> the error kinda looked like uninitalized memory being passed in the 'a' parameter of secp256k1_fe_mul_inner.
14:36 < roconnor> Though it would be more helpful if they said what the UB exactly was.
14:37 < gmaxwell> roconnor: that was also my WAG but I can't tell in which invoation of secp256k1_fe_mul_inner...
14:37 < roconnor> based on the source code <loc> is "*(a + 0)"
14:37 < gmaxwell> It's probably some test stupidity.
14:38 < roconnor> and it means the dereference is the undefined behavior.
14:39 < gmaxwell> oh it's saying a is uninit not just the memory pointed to by it being uninitilized?
14:39 < roconnor> wierd.
14:40 < gmaxwell> I'm running with -trace now... but it outputs two lines for every executed statement
14:40 < roconnor> *lol* This is the function that I proved corrected with VerifiableC.
14:40 < roconnor> *proved correct
14:41 < gmaxwell> I would totally believe the tests run a fe multiply on uninitilized memory, but not with a bad pointer.
14:42 < gmaxwell> (as valgrind and friends won't complain about using an uninitilized value unless control flow ultimately depends on it)
15:02 < real_or_random> maybe "*(a + 0)" was reduced into <loc> already, where <loc> is some memory location
15:03 < real_or_random> (implying that the problem is not a but the memory pointed to by a)
15:04 < gmaxwell> okay, well that would be better news. (obviously the test shouldn't be doing that either, but it wouldn't be too surprising to me if it did)
15:06 < real_or_random> you should see it at the end of the -trace :D
15:17 < real_or_random> hm I don't think that *a is uninitialized. that should be caught earlier by VERIFY_BITS(a[0], 30)
15:19 < roconnor> depends on if VERIFY_BITS is disabled.
15:19 < roconnor> (I disabled it when I doing my verification)
15:39 -!- sipa [~pw@gateway/tor-sasl/sipa1024] has quit [Remote host closed the connection]
15:39 -!- sipa [~pw@gateway/tor-sasl/sipa1024] has joined #secp256k1
16:13 < gmaxwell> I had to turn off VERIFY because of the UB I mentioned before.
16:13 < gmaxwell> It's shifting a value larger than the the size of its type.
16:13 < gmaxwell> 14:16:40 < gmaxwell> Stuck state: in function secp256k1_fe_sqr_inner, expression !(25U >> 38 == 0)
16:14 < gmaxwell> trade is too darn slow
16:14 < gmaxwell> gonna insert printfs and bisect the codebase.
16:25 < gmaxwell> it's inside     secp256k1_context *sign = secp256k1_context_create(SECP256K1_CONTEXT_SIGN);
16:36 < gmaxwell> in secp256k1_ge_set_all_gej_var
16:45 < gmaxwell> sense. this makes none.
16:47 < gmaxwell> it's happening in the block with the comment "Use destination's x coordinates as scratch space" when i=0, but when i=0 there is no femul
17:00 < gmaxwell> I think ccomp is just broken. It's showing the fe_mul being run when last_i == SIZE_MAX.
17:01 < gmaxwell> As in a put a print inside the else clause that prints last_i and it shows it being SIZE_MAX, which is impossible.
17:15 < gmaxwell> Am I being stupid? ccomp says last_i != SIZE_MAX   after size_t last_i = SIZE_MAX;
17:15 < gmaxwell> does SIZE_MAX not fit in size_t or am I on drugs?
17:20 < gmaxwell> looks like it's somehow managed to get an incorrect definition of SIZE_MAX wrt size_t
17:26 -!- instagibbs [~instagibb@pool-100-15-135-248.washdc.fios.verizon.net] has quit [Ping timeout: 258 seconds]
17:52 < gmaxwell> also the earlier claim about "(25U >> 38 == 0)" being undefined is just wrong, the type on the left is uint64_t, there is nothing wrong with shifying it right by 38.
17:55 -!- instagibbs [~instagibb@pool-100-15-135-248.washdc.fios.verizon.net] has joined #secp256k1
17:59 -!- belcher [~belcher@unaffiliated/belcher] has joined #secp256k1
18:05 < roconnor> gmaxwell: can you maybe try breaking size_t last_i = SIZE_MAX; into two statements.
18:06 < gmaxwell> K, running, I expect it'll claim the assignment overflows.
18:06 < gmaxwell> I think I've got some header mismatch problem.
18:08 < roconnor> I'm really not expecting my suggestion to change anything.
18:09 < roconnor> what was the arch you are on again?
18:10 < gmaxwell> PPC64.
18:11 < gmaxwell> (I still don't have a result for you yet, it takes a long time for the interp to get anywhere.)
18:12 < roconnor> so you are compiling for a PPC32 bit target?
18:12 < roconnor> I mean, I know we are running the interpreter.
18:12 < roconnor> Just trying to understand what an unsigned long (size_t) is.
18:13 < gmaxwell> right! so my compcert binary initially was built for ppc64 target, but I recompiled it for ppc32 in case that was the issue.
18:13 < roconnor> ... and it doesn't matter because even if SIZE_MAX is getting trucated or other stipid things under compcert it would still end up with the correct value.
18:14 < gmaxwell> splitting the line didn't change anything.
18:14 < gmaxwell> like I have this:
18:14 < gmaxwell>     size_t last_i;
18:14 < gmaxwell>     last_i = SIZE_MAX;
18:14 < gmaxwell>     printf("weee %s %d last_i == SIZE_MAX = %d\n",__FILE__,__LINE__,last_i == SIZE_MAX);
18:14 < gmaxwell> and interp outputs
18:14 < gmaxwell> weee src/group_impl.h 134 last_i == SIZE_MAX = 0
18:16 < roconnor> okay well that could happen if the SIZE_MAX value is getting truncated.
18:16 < roconnor> from 2^64-1 to 2^32-1
18:16 < roconnor> I mean if SIZE_MAX is 2^64-1 but size_t is a 32-bit unsigned int.
18:17 < roconnor> which in turn could happen from header confusion.
18:19 < gmaxwell> [gmaxwell@argonaut secp256k1]$ cat wetest.c
18:19 < gmaxwell> #include <stddef.h>
18:19 < gmaxwell> #include <stdint.h>
18:19 < gmaxwell> #include <stdio.h>
18:19 < gmaxwell> int main(int argc, char ** argv) {
18:19 < gmaxwell>   size_t x;
18:19 < gmaxwell>   x = SIZE_MAX;
18:19 < gmaxwell>   printf("%d\n",x == SIZE_MAX);
18:19 < gmaxwell>   return 0;
18:19 < gmaxwell> }
18:19 < gmaxwell> [gmaxwell@argonaut secp256k1]$ ccomp -random -interp wetest.c
18:19 < gmaxwell> 0
18:19 < gmaxwell> Time 20: observable event: extcall printf(& __stringlit_1, 0) -> 2
18:19 < gmaxwell> Time 27: program terminated (exit code = 0)
18:19 < roconnor> But I don't really know how "#include <stdint.h>" could end up confused.  I suppose if compcert isn't well designed it might end up confused.
18:20 < roconnor> want to printf("%ld; %ld", sizeof(size_t), SIZE_MAX) ?
18:20 < gmaxwell> yeah, I just checked size_t, 4 bytes
18:21 < roconnor> maybe pritnf("%lld", (unsigned lond long)SIZE_MAX) to be safe.
18:22 < gmaxwell> -1  it claims it's called with -1LL
18:23 < gmaxwell> (and sizeof long long is 8)
18:23 < gmaxwell> so it just has header confusion of some kind.
18:24 < roconnor> well that's kinda a relief.
18:27 < gmaxwell> maybe that it's just never been tested running on a ppc64le host, presumably the authors mostly crosscompile to ppc.
18:27 < gmaxwell> (e.g. some of the most common chips for spacecraft are ppc)
18:28 < roconnor> I remember some wonkiness trying to get x86-32 compiled on a x86-64 machine.  This sort of stuff is a bit beyond my pay grade though.
18:29 < roconnor> I don't really understand computers.
18:29 < gmaxwell> well duh, like anyone else does?
20:24 < midnightmagic> i knew a guy once. i think he understood computers.
20:24 < midnightmagic> he disappeared and we never heard from him again
22:33 < gmaxwell> seems to work better on x86_64 though this host only has 128 GB ram...
--- Log closed Thu May 16 00:00:14 2019