4 ms·
What happens if a function allocates not deterministically, like if (turing_machine_halts(tm)) return malloc(1); else return NULL; How is this handled?
by thealistra 9mo ago
What happens if a function allocates not deterministically, like
if (turing_machine_halts(tm)) return malloc(1);
else return NULL;
How is this handled?
- jonhohle 9mo agoNULL is a valid return for malloc. Wouldn’t that case already be handled?
- dnautics 9mo agoas someone building an analyzer for zig, if you sent something like this through the system im building, it would get handled by Zig's optional type tagging; but lets say you did "free" (so your result is half freed, half not freed): it would get rejected because both branches produce inconsistent type refinements, you don't have to solve the halting problem, just analyze all possible branches and seek convergence.
- dwattttt 9mo agoRust is the poster child for these complaints, but this is a great example of "the language rejects a valid program". Not all things that can be expressed in C are good ideas! This is "valid" C, but I wholly support checking tools that reject it.
- dnautics 9mo agoexactly! "guaranteeing the safety of C" sir what did you think that meant, sprinkling magic fairy dust to make it work!!?
- dnautics 9mo agoi made a quip and realized that's not a bad description of what fil-c does
- throwaway17_17 9mo agoAre you implying that Fil-C has this sort of reaction to people confused about why it does certain things in the name of safety, or are you saying Fil-C is just sprinkling magic fairy dust on C and declaring it safe?
- dnautics 9mo agoi like fil-c, so i would say "fil c sprinkles magic fairy dust on C and makes it safe (at the cost of perf and elevated risk of crashing)
- SkiFire13 9mo ago> just analyze all possible branches and seek convergence. This sounds like a very simple form of abstract interpretation, how do you handle the issues it generally brings? For example if after one branch you don't converge, but after two you do, do you accept that? What if this requires remembering the relationship between variables? How do you represent these relationships? Historically this has been a tradeoff between representing the state space with high or perfect precision, which however can require an exponential amount of memory/calculations, or approximate them with an abstract domain, which however tend to lose precision after performing certain operations. Add dynamically sized values (e.g. arrays) and loops/recursion and now you also need to simulate a possibly unbounded number of iterations.
- dnautics 9mo ago> For example if after one branch you don't converge, but after two you do, do you accept that? you should refactor so that it's representable. > Add dynamically sized values (e.g. arrays) and loops/recursion and now you also need to simulate a possibly unbounded number of iterations. regions are hard. You kinda have to reject regions that are not uniform. loops you can find a fixpoint for.
- RossBencina 9mo agoIn general, symbolic execution will consider all code paths. If it can't (or doesn't want to) prove that the condition is always true or false it will check that the code is correct in two cases: (1) true branch taken, (2) false branch taken.
- thealistra 9mo agoI understand how this works in general. I had static analyzers at Uni, I know lattice theory and all this - I am just wondering how Xr0 handles it.
- tgv 9mo agoI think all paths have to return the same allocation. You would have to solve this in another way.
- thealistra 9mo agoIsn’t this a very restrictive way to write? Hard for me to imagine as never wrote with such annotations so no idea how viable it is for a large codebase to have this constraint.
- tgv 9mo agoSure, but you want restrictions. You can't get an annotation that magically eliminates (de)allocation errors. It comes at a cost. The advantage of this particular proposal is its simplicity, I think. Otherwise, you'd have to get into contracts with complex expressions and then you'll have to prove those expression hold, and before you know it, your program is filled with proof statements. At least, that's my (limited) experience in SPARK, where you even can't have pointers.
- thealistra 9mo agoMy point is can you write a json deserializer with this, where allocation of every child is defacto optional, depending on input JSON?
- fc417fc802 9mo agoAs long as the verifier can be satisfied by wrapping the different results in a common type you should be fine. There has to be some way to appease it in that scenario as otherwise even trivial programs wouldn't be able to pass.
- nextaccountic 9mo agoThere will always be valid programs that are nonetheless rejected by some verifier (Rice's theorem). That is, programs that have really nothing wrong but nonetheless are rejected as invalid In those cases you generally try to rewrite it in another way