Gecode won the minizinc challenges from inception of the challenge in 2008 until 2012, but these days or-tools wins gold every year 2013 to 2024, and in 2024 swept gold in all categories.
Why is gecode interesting? Why use it over or-tools?
229 karma · joined May 1, 2019
Why is gecode interesting? Why use it over or-tools?
E-matchers are an algorithm over e-graphs to efficiently search for a pattern in an e-graph, for instance if you want to find "(load ptr) * (load ptr)" then you have to find "#x * #x" for all x in all e-classes, then check whether "load ptr" is a member of e-class #x. This is where you get limits on what you can match. "Pattern matching" style transforms are easy and fast using e-matchers, things like "x * 2" -> "x << 1", but beyond that they don't help.
There's an optimizer problem where you have "load ptr" and you solve ptr and figure out it's pointing to a constant value and you replace the load instruction with the constant value. Later, you get to code emission and you realize that you can't encode your constant in the CPU instruction, there's not enough bits. You now need to take the constant and stuff it into a constant pool and emit a load for it. If you had stored them in an e-graph, you could have chosen to use the load you already had.
Suppose you wanted to do sparse conditional constant/constant-range propagation but your IR uses an e-graph. You could analyze each expression in the e-class, intersect them, and annotate the resulting constant-range on the whole e-class. Then do SCCP as normal looking up the e-class for each instruction as you go.
FWIW, I think this should be considered a language design problem rather than an optimizer design problem. Black box optimizer behaviour is good for enabling language designs that have little connection to hardware behaviour, and good for portability including to different extensions within an ISA.
C doesn't offer a way to express any timing guarantees. The compiler, OS, CPU designer, etc. can't even do the right thing if they wanted to because the necessary information isn't being received from the programmer.
Could you defend the statement that "foundem" is a scam? If it really was then that adds important context to the ruling, but I'll need something more concrete than hyperbole.
> That's a lie.
All C functions return via a return statement with expression (only for non-void functions), a return statement without an expression (only for void functions) or by the closing of function scope (only for void functions). True?
The simple "spit out a block of assembly for each thing in the C code" compiler spits out the epilogue that works for void-returning functions, because we reach the end of the function with no return statement. That epilog might happen to work for non-void functions too, but unless we specify an ABI and examine that case, it isn't guaranteed to work for them. So it's not correct to emit it. True?
Where's the lie?
> > Adding runtime checks for the UB case is ignoring? Having the compiler find the UB paths to insert safety code is ignoring?
> Don't come onto HN with the intent of engaging in bad faith.
Always! You too!
The text you quoted was referring to how real compilers handle falling off the end of a non-void function today with -fsanitize=return from UBSan. If I understand you correctly, in your reading a compiler with UBSan enabled is non-conforming because it fails to ignore the situation. That's not an argument as to whether your reading is right or wrong, but I do think UBSan compilation ought to be standard conforming, even if that means we need to add it to the Standard.
To the larger point, because the Standard doesn't define what "ignore" means, the user and implementer can't use it to pin down whether a given UB was ignored or not, and thus whether a given program was miscompiled or not. A compiler rewrites the code into its intermediate IR -- could be Z3 SMT solver or raw Turing Machine or anything -- then writes code back out. Can ignoring be done at any stage in the middle? Once the code has been converted and processed, how can you tell from the assembly output what's been ignored and what hasn't? If you demand certain assembly or semantics, isn't that just defining undefined behaviour? If you don't demand them, and leave the interpretation of "ignore" to the particular implementation of a compiler, yet any output could be valid for some potential design of compiler, why not allow any compiler emit whatever it wants?
FWIW, there once was a real good-faith effort to clean up the problems, Friendly C by Prof Regehr, https://blog.regehr.org/archives/1180 and https://blog.regehr.org/archives/1287 .
It turns out it's really hard. Let's take an easy-to-understand example, signed integer overflow. C has unsigned types with guaranteed 2's complement rules, and signed types with UB on overflow, which leaves the compiler free to rewrite the expression using the field axioms, if it wants to. "a = b * c / c;" may emit the multiply and divide, or it can eliminate the pair and replace the expression with "a = b;".
Why do we connect interpreting the top bit as a sign bit with whether field axiom based rewriting should be allowed? It would make sense to have a language which splits those two choices apart, but if you do that, either the result isn't backwards compatible with C anyways or it is but doesn't add any safety to old C code even as it permits you to write new safe C code.
Sometimes the best way to rewrite an expression is not what you'd consider "simplified form" from school because of the availability of CPU instructions that don't match simple operations, and also because of register pressure limiting the number of temporaries. There's real world code out there that has UB in simple integer expressions and relies on it being run in the correct environment, either x86-64 CPU or ARM CPU. If you define one specific interpretation for the same expression, you are guaranteed to break somebody's real world "working" code.
I claim without evidence that trying to fix up C's underlying issues is all decisions like this. That leads to UBSan as the next best idea, or at least, something we can do right now. If nothing else it has pedagogical value in teaching what the existing rules are.
Most of the time people accuse compilers of finding and exploiting UB and say they wish it would just emit the straight-forward code, as close to writing out assembly matching the input C code expression by expression as possible. Here you have an example where the compiler never checked for UB let alone proved presence of UB in any sense, it trusted the user, it acted like a high-level assembler, yet this compiler is still not ignoring UB for you? What does it take? Adding runtime checks for the UB case is ignoring? Having the compiler find the UB paths to insert safety code is ignoring?
https://www.chicagomanualofstyle.org/qanda/data/faq/topics/C... https://www.cjr.org/language_corner/out_of_range.php
The wording change from Permissible to Possible and making it non-normative was an attempt to clarify that the list of behaviors that follows is a false range and not an exhaustive list.
It's a submarine change because in the eyes of the committee, this is not a change, merely a clarification of what it already said, to guard against ongoing misinterpretation.
I agree with you, but is there any peer-reviewed publication that can be cited? The idea makes sense to me, firstly the Reals \ Inaccessible Reals = Computable Reals, secondly you can't ever input an inaccessible real to an experiment nor retrieve one out of an experiment -- but then I'm not completely certain in making the conclusion that no experiment can be devised which shows that inaccessible reals exist in physical space.
I am concerned about this in the field of complexity analysis of quantum computers too, I think that the use of reals in physics is leading to mathematically correct but non-physical results about complexity theory of quantum computers. Having a paper to point at and say "look, stop assuming your Bloch spheres are backed by uncountable sets, it's leaking non-computable assumptions into your analysis of computation" would be helpful.
Not at all! Digital computers can use computable reals which are defined as any function from a rational value (the error bound) to a rational value which is within the supplied error-bounds from the true value. Do not mistake this for computing in the rationals, these functions which perform the described task are the computable real numbers. There are countable-infinity many of these functions, one for each computable real. For instance, note that you can always compare two rationals for equality, but you can't always compare two computable reals for equality, just like reals.
Hans Boehm (of Boehm garbage collector fame) has been working on this for a long time, here is a recent paper on it: https://dl.acm.org/doi/pdf/10.1145/3385412.3386037
ptr->foo = 1;
if (ptr == nullptr)
return;
if (ptr == nullptr)
return;
ptr->foo = 1;Is `printf` allowed to loop infinitely? Its behaviour is defined in the language standard and GCC does recognize it as not being a user-defined function.
As an insider, it was not. The move to zero-trust started with "A new approach to China": https://googleblog.blogspot.com/2010/01/new-approach-to-chin...
Surely not? I mean, you probably didn't intend to include unevaluated contexts like "sizeof(ptr)" where putting in a memory access is forbidden, but I think nearly-all programmers fully expect the compiler to delete the dead store in "ptr = a; ptr = b;" or "ptr = x; free(ptr);" and would get annoyed if it didn't. Especially if we can't just take a scalar computation in a loop, move the memory access to register, then store it to memory only once when we're done.
I once did a cleanup of undefined behaviour dereferencing NULL pointers (-fsanitize=null) and I got a lot of pushback from people complaining about "&ptr" where the ptr is NULL, because the compiler doesn't emit any assembly for that, so their code is just fine as is.
The rule for memory is that all memory you've stored to has an effective-type -- same as the static types but for addresses at runtime -- and a pointer has to point to an object with the effective-type matching the pointer's static type. Further details aside (uninitialized pointers, pointers to data you just freed, freshly malloc'd memory which has no effective type yet, unions) when you think of it in this model, the fact you can't have an int and float* pointing to the memory feels natural.
Can I delete "if (x & 3 == 16)" without a warning? There is no 'x' which makes that expression true, so I can safely fold it to false without a warning?
Can I delete "if (x + 1 < x)" without a warning? There is no signed 'x' which makes that expression true, so I can safely fold it to false without a warning?
How about this:
int x = 7;
call_function_outside_this_file();
if (x != 7) { /* dead */ }
Or this:
void f(int *x, float *y) {
*x = 1;
*y = 2;
if (*x != 1) { /* dead */ }
The problem with UB is that you can use it to set up impossible situations, like create an 'x' where x & 3 == 16 is true or a variable whose address was never taken being modified through a pointer, and so on. If you account for UB then "code that doesn't have a universally defined behaviour" becomes all code.
Ideally I think the first two examples should have warnings, though not because we delete the code, and the last two shouldn't? The warning should be because it's a tautology so the human likely didn't mean to write that (for instance if the human wrote it indirectly through macros, then we shouldn't warn on it).
Neither, pointers are their own types which have no sign, only integral types come in signed and unsigned. There exist intptr_t (signed) and uintptr_t (unsigned) which are integral types you can losslessly cast a pointer to. Also the difference of two pointers is a ptrdiff_t which is a signed integral type.
> The warnings/errors I'd expect would be: *p = 7; // out of known bounds write
In that regard I picked a bad example, this code always executes undefined behaviour, so this could indeed be detected by a compiler warning at the cost of doing a simulated execution of the code. Most real problems come about where the code is UB only for certain runtime inputs.
The reason I chose that example was to make a point about how the compiler doesn't realize it's doing anything to "change" the program, and isn't going out of its way to optimize based on undefined behavior. It assumes that a local variable's value can't change with it being assigned to, so how could it know whether to issue the warning?
Another way to put it is:
void written_in_asm_in_another_file();
void test() {
int x = 4;
written_in_asm_in_another_file();
printf("%d", x);
}
> The pointer math line should still be legal, even if it would be 'unsafe' in some popular other languages.
I'm not sure what you mean by "should", you might be suggesting a change to C or you might be stating what you think the code currently does. Right now in C, the very creation of an invalid pointer is UB whether you use the thing or not. I'm told this is because of very old CPU designs that had distinct pointer and integer registers and loading an invalid address into the pointer register would trap.
It's possible that a program terminating based on attacker influenced values could be used as a channel to leak confidential data to the attacker, so I'd suggest that developers decide whether to use this on a case-by-case basis. (Maybe it should default to on, but we'd need user education so people who are building sensitive systems know they need to turn it off.)
Can I ask you, have you tried any existing tools? Coverity static analysis, Klocwork, PVS-Studio, clang static analysis, tis-interpreter, Frama-C? What did you think of those? If not, why not (how important is the problem to you)?
My understanding of these tools is that they start by marking every spot potential UB could happen -- every add is potentially overflowing, every pointer dereference is potentially null or freed or whatnot, and then they use solvers to prove that the UB does not occur, and print out the rest. The benefit they have is that they can examine more than one file at a time (the compiler may only look at one .c file at a time) and they have permission to take much longer than compiling.
> -Wubelim # Warn any time code is eliminated as a result of undefined behavior / assumptions.
This doesn't happen, the compiler doesn't detect your UB and use that to delete your code. Consider this:
int x = 4;
int y;
int *p = &y - sizeof(int);
*p = 7;
printf("%d", x);
Another way to think about it is that the assumptions we make about your program being free of UB are completely indistinguishable from all the rest of the correct and working code. "int x = 4;" should declare a new variable, named x, with an int's worth of memory, initialized to the value 4. That is precisely as true to the compiler as any UB-performing, code. When you write "p->xcoord" you are telling the compiler that 'p' is a valid pointer to an object of its type at this moment, and it believes you. Trust the programmer, and all that.
> -Wub... # Any other classes of UB optimizations that change the program as (incorrectly) written.
"UB optimizations" isn't a thing. It just isn't. The optimizations never change the program, at least, not unless the compiler is buggy. The compiler's job is to find some assembly which meets the specification we call the program. With the optimizer enabled, we spend more time so that we can select assembly that minimizes a cost model we have for the execution time on the underlying machine (or sometimes file size).
> Again, the goal is to provide feedback that improves the program and possibly educates / reminds the programmer about how their meanings might be misunderstood.
FWIW we agree on the goal.
The model for warnings in clang at least has been to look at the code as it is typed, and focus on errors that programmers make. We have all kinds of complex rules for warnings, like "if (3 < 4)" issues a warning (-Wtautological-compare) but "if (MAX_THREADS < MAX_CORES)" with #define MAX_THREADS 3 and #define MAX_CORES 4 doesn't. We've put a ton of effort into getting this sort of thing right, and that includes warnings that code will always produce UB when run, even if it was expanded through macros or templates. It's not an exhaustive system, the warnings work was guided by actual bugs we've encountered in real systems.
There might be another way to do this. The C++ constexpr feature has the compiler evaluate some functions at compile time and detect any UB they encounter as they run. The clang implementation of this can also handle working with values that are not known at compile time, and working with dynamic allocations. One could try to run every function with the constexpr evaluator and see whether it does a better job at producing good warnings, then remove the redundant warnings (made by pattern matching on the AST) and see if the result is fast enough to use as part of regular compilation.
vector<t> v;
v.push_back(a);
v.push_back(b);
v.push_back(c);
v.push_back(d);
template <typename T> struct vector<t> {
size_t len = 0;
size_t storage_len = 0;
T *storage = nullptr;
void push_back(T t) {
if (len + 1 > storage_len) {
storage_len = storage_len ? storage_len * 2 : 1;
storage = realloc(storage, storage_len);
}
storage[len] = t;
++len;
}
};
vector<t> v;
v.push_back(a);
v.push_back(b);
v.push_back(c);
v.push_back(d);
len = 0;
storage_len = 0;
storage = nullptr;
if (len + 1 > storage_len) {
storage_len = storage_len ? storage_len * 2 : 1;
storage = realloc(storage, storage_len);
}
storage[len] = a;
++len;
if (len + 1 > storage_len) {
storage_len = storage_len ? storage_len * 2 : 1;
storage = realloc(storage, storage_len);
}
storage[len] = b;
++len;
if (len + 1 > storage_len) {
storage_len = storage_len ? storage_len * 2 : 1;
storage = realloc(storage, storage_len);
}
storage[len] = c;
++len;
if (len + 1 > storage_len) {
storage_len = storage_len ? storage_len * 2 : 1;
storage = realloc(storage, storage_len);
}
storage[len] = d;
++len;
len = 0;
storage_len = 0;
storage = nullptr;
if (0 + 1 > 0) {
storage_len = 1;
storage = realloc(storage, 1);
}
storage[0] = a;
len = 1;
if (1 + 1 > 1) {
storage_len = 2;
storage = realloc(storage, 2);
}
storage[1] = b;
len = 2;
if (2 + 1 > 2) {
storage_len = 4;
storage = realloc(storage, 4);
}
storage[2] = c;
len = 3;
if (3 + 1 > 4) {
storage_len = 8;
storage = realloc(storage, 8);
}
storage[3] = d;
len = 4;
bool overflowed = (x+1)<x;
Nevertheless, I don't know what to do about the suggestion "it may or may not do what you want on any given architecture, but it shouldn’t just be assumed false." The compiler needs to know what it can and can't do. The common advice of "just do what the CPU does" doesn't work, we need to know what to do when cross-compiling, when constant folding, and we need to know which instructions are valid to select. If I selected PADDSW for this add (a saturating addition operation) but then later when you use x+1 I select a non-saturating addition, would you be happy with that? Probably not. The compiler needs actual rules to follow.
I don't know how to apply the suggestion about warnings when we end up deleting dead code. The compiler deletes dead code all the time, consider a case like "vector<t> v; v.push_back(a); v.push_back(b);", each push_back begins with an if-statement on whether reallocation is required, and that becomes constant with inlining. Tracking "this code became dead because", well, because which situations exactly?
Would you like warnings on:
* int f(int x, int y) { return x + y; }
* int get_x_coord(Point *p) { return p->x; }
* void compute_and_cache(const char *key) { *get_cache_bucket_for(key) = compute_value_for(key); }
On the flip side, I can offer -fsanitize=undefined which will catch when you do many things that have UB at runtime. It does not change the ABI which means that there are some bugs it can't catch, but deploying it is easier since you do not need to recompile all your libraries with it (like your C++ standard library and C library, in particular). You can use this to help you build unit tests that send intentionally overflowing values into your functions and show that they do not overflow. It turns untestable problem (since you cannot check for UB after it happens) into a problem you can write deterministic tests for.
> - “np” - a category of problems which can be checked, but not solved, in O(n²)
These definitions are incorrect. Certainly there are other polynomials than just n². P is the complexity class wherein the problem can be solved on a Turing machine in a number of steps equal to some polynomial of the size of the input. For NP, replace "Turing machine" with "nondeterministic Turing machine" and otherwise it's the same. The 'size of the input' is the count of symbols on the machine's tape, allowing for the input to be written in any finite alphabet, chosen by the designer of the Turing machine.
Nondeterministic can mean different things in different contexts, so I want to clarify. Here, nondeterministic means that the machine does the 'impossible' thing of forking itself and running up to an infinite number of copies of the deterministic machines (including distinct copies of their state) at the same time, then if one of the computations succeeds then that computation is kept and the others are discarded (including the count of how many steps they spent). This is why, if you have a machine that can check a problem in P, you can make the machine to solve it in NP by wrapping your checker in "use nondeterminism to generate every possible input value" and simultaneously check them all.
I highly recommend the theory of computation course at MIT, which is freely available online:
https://ocw.mit.edu/courses/18-404j-theory-of-computation-fall-2020/
https://www.youtube.com/playlist?list=PLidiQIHRzpXIFFbyGrWkqXXVj0BztDcTF
> All information necessary to generate checkable solutions to any problem must be encoded in the problem itself, or the problem would be undecidable, because there would be no way to check a solution against a problem if the problem and solution were completely unrelated.
This is actually a great insight, but you must keep in mind that if I tell you that the solution to "a > b" is True, you cannot find a and b. You are touching on an important concept in computer science theory called "reversible computing". It's also related to information theory. If I have a machine that solves the travelling salesman problem that outputs "the fastest route is from B to C to A", then you must ask yourself whether there are multiple different inputs to the problem which can generate that output? (You don't always have the freedom to change the input type of the problem, or else I could factor integers in constant time by demanding that all integers must be input as a product of primes.)
When the values are computable from the other, the question remains about the number of steps it takes to do. You still have to show that it's bounded above by some polynomial, and then that this is true for all problems in NP. We already have ways to rewrite one NP problem into another, and so showing a single machine that takes polynomial steps to solve any of those NP problems would suffice to show that P = NP. This is how we've proven lots of complexity classes the same in the past. On the other hand, we have almost no techniques which prove that two complexity classes are distinct.
Also! While the usual sanitizer runtime libraries aren't security hardened for use in production environments, but for UBSan there's -fsanitize-minimal-runtime which switches to a different runtime library that is intended for this purpose (or use -fsanitize-trap=... instead, which executes an illegal instruction on error). Note that if your program terminates with a UBSan error, an attacker who can check whether your program terminated or not could use that as a primitive to leak data, so consider the security impact on your use case carefully. UBSan has a quite small performance impact when building with optimization, so you could deploy to production with it enabled, or parts of it enabled.
You can mutate a vtable without UB. A method may call the destructor on its this pointer and use placement-new to create a new object in place. The fact that any method of a class may do this combined with the fact that the placement-new object might be a more derived version of the destroyed object (so an existing Foo* continues to be valid) means that compiler can't cache vtable lookups for consecutive method calls, making nearly any optimization of virtual function calls impossible because you don't know the type or called function, unless you see the object being constructed (when the vptr is assigned) and inline each called function in turn.
(At some point C++ added a rule that basically reads "you're allowed to cache the vptr, if the accesses were written using the same pointer variable name". This doesn't work well for optimizing compilers because they'll quickly fold two equal values into a single variable in their internal languages and lose track of whether the user wrote two distinct variable names or not.)
You moved a _little_ too quickly.
There exist program-pairs which can be proven equal, and those for whom no proof exists. You can organize the production of new programs into finite steps and organize the act of creating a proof-of-equivalence between the input and output into finite steps, then execute one step of creating a new program candidate followed by one step of finding the equivalence proof for each of the (finite number of) candidate programs created so far. In this way you are guaranteed to find an output program and its equivalence proof whenever such an (input-program, output-program, equivalence-proof) tuple exists.
Finding the equivalence proof is recursive enumeration—the same as creating the program candidates—but in some machine verifiable proofing language.
Speeding this up by leaving out syntactically incorrect programs and equivalent programs, as well as defining the proofing language and implementing the checker are left as an exercise to the reader.