Comment by thealistra
4 days 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?
4 days 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?
NULL is a valid return for malloc. Wouldn’t that case already be handled?
In 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.
I 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.
as 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.
Rust 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.
exactly! "guaranteeing the safety of C" sir what did you think that meant, sprinkling magic fairy dust to make it work!!?
3 replies →
> 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.
> 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.
There 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
I think all paths have to return the same allocation. You would have to solve this in another way.
Isn’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.
Sure, 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.
2 replies →