16 ms·

Xr0: C but Safe

• deleted 3y ago
  [deleted]
• compressedgas 3y ago
  Looks like it's a C version of Dafny.
  • akiarie 3y ago
    A lot of truth to this. (Speaking as one of the creators of Xr0).
• gpderetta 3y ago
  It is quite interesting, but it seems to fail with even very simple examples: void x() { int * p; p = malloc(1); if(0) { free(p); } else { free(p); } } 0v: src/ast/stmt/verify.c:228: stmt_sel_exec: Assertion `!ast_stmt_sel_nest(stmt)' failed.
  • masklinn 3y ago
    To be fair if the program never runs it’s 100% safe.
  • akiarie 3y ago
    Good spot. We hadn't enabled `else` last week when we posted, but we've just fixed this [0]. [0] https://github.com/xr0-org/xr0/releases/tag/v0.15.0 https://github.com/xr0-org/xr0/releases/tag/v0.15.0
    • gpderetta 3y ago
      Very nice. I was worried that conditionals would confuse it. But this passes: void x(int f) { int * p; p = malloc(1); if(f) { free(p); } if(!f) { free(p); } } And this doesn't, as expected: void x(int f) { int * p; p = malloc(1); if(f) { free(p); } if(f) { free(p); } } edit: another assertion failure: void x(int f) { int * p; p = malloc(1); if(f) { free(p); } f = !f; if(f) { free(p); } }
      • akiarie 3y ago
        This is another good spot. Xr0's logical/arithmetic analysis is currently limited because we've been more focused on getting the structures of the language working as a whole. So you'll get more of these asserts if you try using `&&`, ternaries, and so on. We've put a fix in for this on a dev branch for now though: https://github.com/xr0-org/xr0/issues/43 https://github.com/xr0-org/xr0/issues/43
        • gpderetta 3y ago
          This seems very hard in general to fix: void x(int a, int b) { int * p; p = malloc(1); if(a) { free(p); } if(b) { free(p); } } It is possible that the program always guarantees that a!=b, but it would be hard to prove even with whole program analysis. Are you planning additional annotations or this is just not expected to work?
          • mst 3y ago
            I can't speak for the authors but I think I'd file that one under "and if you write this, ideally a small gnome exits the back of the computer and hits the developer with a mallet." I'd be perfectly happy refactoring that so I could have an 'a or b' test (I'm assuming $something means that x(0, 0) not free-ing is correct in real code because nitpicking an illustrative example would be silly). Though note that I'm sufficiently bad at tracking things right when writing C that I tend to spend most of my debugging time figuring out what stupid mistake I made to cause the current segfault - so I'm probably more willing than average to write code differently if it helps me avoid that ;)
          • akiarie 3y ago
            This is another good find. We haven't yet implemented the `!=` operator (or most of the binary operators). Incidentally, you will notice that Xr0 rejects the program as is, which is correct (because of the double free). It can, however, accept code like the following: void foo(int a, int b) { int *p; p = malloc(1); if (a) { if (!b) { free(p); } } if (b) { free(p); } if (!a) { if (!b) { free(p); } } } I say "can" because we only have this working on a development branch [0], and there are still some issues we're resolving on this, hopefully by next week. [0]: https://github.com/xr0-org/xr0/tree/fix/nested-branching https://github.com/xr0-org/xr0/tree/fix/nested-branching
  • PennRobotics 3y ago
    Plus, at -O1 and up, gcc optimizes this away, so the check itself is not well-defined as necessary. Does it always make sense to strictly enforce code that will be optimized/changed during compilation? Or does Xr0 run after compilation/linking? How to handle things like unions where you want data in a nice mixed-type struct that is used locally and can also be sent as a stream of uint8_t over a wireless connection? Then, the last function that needs to use the memory frees it. Or is that still fine as long as you malloc once somewhere, free once somewhere, and annotate that the memory region will be accessed as more than one dereferenced type? Much more important: Will the proposed changes be understandable enough for your average CS undergrad to learn in four months of halfway diligent study? (Then again, you might do away with students taking time to debug improper malloc/free and whatever else falls under the scope of Xr0...)
    • gpderetta 3y ago
      the if(0) was just to minimize the test case. if(variable) also fails. This doesn't need to be perfect though. Just incrementally better than the status quo.
• zamalek 3y ago
  This seems vaugely similar to C# Code Contracts. The difference there is that it was embedded as an assertion into the method: Contract.Requires(start > 0); Contract.Ensures(someReturn != null); I loved it. It gave you much (not all) of that "if it compiles it works" good vibes that Rust has. Though, oh boy, were you in for a surprise if you think that Rust compiles slowly. You could probably do something similar with C: CONTRACT_REQUIRE(x == 0 || x == -1); if(x) { void* result = malloc(1); CONTRACT_ENSURE(result != null); CONTRACT_CALLER(free(result)); return result; } else { CONTRACT_ENSURE(result == 0); return 0; } The nice thing about that is you could have a compatibility .h that asserts/nops the macros, making the code compile in ignorant compilers.
  • thesuperbigfrog 3y ago
    You can use "Design by Contract" (https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Design_by_contract) in Rust: https://docs.rs/contracts/latest/contracts/ https://docs.rs/contracts/latest/contracts/ Ada has Design by Contract built into the language (not a library): https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... DbC is awesome because it formalizes what conditions must exist before and after a piece of code runs and defines who (caller vs. callee) is responsible for what parts.
• eqvinox 3y ago
  Making the annotations something the standard C preprocessor can remove would be great. Some word plus braces. So you can compile as normal C.
  • zokier 3y ago
    Frama-C uses comments for annotations: https://frama-c.com/html/acsl.html https://frama-c.com/html/acsl.html
• sitkack 3y ago
  This is awesome! Though if one wants C and safety and a great language you can get there via, Rust -> Wasm -> C (via wasm2c). It would be cool to see this applied to say, rsync.
• vintermann 3y ago
  There are earlier attempts to do this, CCured was as I recall wholly based on comment annotation, and it was also closely related to cyclone, which inspired rust. Have you looked at them? Always good to look at prior art, it's not easy what you're trying to do.
  • bvrmn 3y ago
    Prior art is hard to find and touch in-person. There is real reason the only easy searchable leftovers are academic papers.
    • vintermann 3y ago
      Well I mentioned some, at last. Pretty sure I still have the CCured code lying around in a backup somewhere, I downloaded it and played with it long ago. If it's truly not available on the net anywhere, I suppose I can try to dig it up.
• Locke80 3y ago
  You can also have this with nice looking syntax: the projects are called swift and rust.
• rq1 3y ago
  What’s the difference between what you’re trying to achieve and what ATS already did? The syntax?
• meatjuice 3y ago
  Do you think C has a better syntax compared to Rust? I'm honestly not sure about this. It surely heavily depends on your preferences, though. Generally speaking, what do you think?
  • burjui 3y ago
    It has a generally simpler syntax, except for function pointers and arrays, but I wouldn't call it "better". Comparing syntaxes of such different languages is pointless anyway. Syntax should serve semantics.
    • akiarie 3y ago
      "Simpler" is the word that we care about. Although Rust is an advance on C in many significant ways, what it loses is the simplicity. One of our goals is to offer three same advances (and more) but without compromising on simplicity.
• irq-1 3y ago
  If 0v can tell what the abstract needs to be, why do we need to write it down? It has to know the abstract to compare against the annotation. Maybe it's so we better understand the origin of the problem, rather than getting 'free error' at the end of a long chain of functions?
  • akiarie 3y ago
    It cannot in general deduce the abstract. Doing so would require solving the halting problem.
    • muldvarp 3y ago
      It also can't in general deduce whether the abstract and the implementation match, as doing so would require solving the equivalence problem (which is undecidable for anything as or more powerful than pushdown automata).
      • akiarie 3y ago
        I'm not very familiar with the equivalence problem, but at least for Xr0 abstracts (what we call the annotations attached to functions & loops) there is an extremely strong structural similarity between the implementation and the annotation. So it's not at all clear that we'll run into this.
        • muldvarp 3y ago
          > there is an extremely strong structural similarity between the implementation and the annotation. If the annotation is basically just a copy of the function body why have any annotation at all? > So it's not at all clear that we'll run into this. It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this.
          • akiarie 3y ago
            > If the annotation is basically just a copy of the function body why have any annotation at all? This is a profound question. Xr0 annotations seem to be copies of the function bodies, but they aren't actually. What they are is a description of the function's safety semantics, the side effects and circumstances under which the function may be relied upon to exhibit well-defined behaviour (under the C Standard). They only seem to be copies of the bodies because we're dealing with simple examples in the post here and in the tutorial, but we have a much more significant program ready (documenting) that we'll be sharing soon that shows the difference more clearly. Xr0 is built in explicit reliance upon the powers of programmers to structure code in such a way that the annotations become simpler and simpler as you move up layers of function abstraction. As a simple example, think about what happens when you allocate memory and free it within a function, e.g. #include <stdlib.h> void foo() ~ [ return malloc(1); ] { return malloc(1); } void bar() { void *p = foo(); free(p); } void baz() { bar(); /* completely safe */ } Note that `foo`'s annotation is like a copy of its body, but `bar`'s annotation is very simple, even though it interacts with `foo`, which is only safe if the pointer it returns is handled. So from `baz`'s perspective there are no safety semantics it has to worry about when it interacts with `bar`. The complexity that could lead to safety bugs in `foo` has been completely handled in `bar`. We call this simplifying phenomenon denouement, and well-designed programs exhibit it very strongly. Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0. > It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this. Yes, but we don't. Only well-defined behaviour according to the C Standard. This is the goal for Xr0 v1.0.0. After that the sky is the limit.
• moody__ 3y ago
  Interesting idea but I have some issues with the code style here. Two problems I see are implicit casts from pointers to integers and use of func() instead of func(void). These are both somewhat minor complaints but they tend to lead to bugs when tested in other environments. In this case I would expect a project aiming to be "C but safe" would at least take the maximum use of existing C safety features. Also the annotations seem a bit cumbersome, I know that's easy to say without providing an alternative but something just doesn't sit right with me about how verbose they are.
  • akiarie 3y ago
    Interesting points. Because it's easy to do the type checking at compile time for function prototypes (though we haven't implemented it yet) we haven't felt under pressure to use the `func(void)` notation, which has always felt somewhat uncouth to me. The verbosity of the annotations is the most jarring thing at the beginning. However, do you find any of them unclear? Because we're optimising for similarity to C before terseness.
    • moody__ 3y ago
      I don't find them unclear at all, after reading the introduction I felt pretty comfortable with everything that was going on in the examples. I think this type of approach you're going for can work depending on how it grows to cover more complex cases like loops. I'll be keeping tabs on how your work progresses.
• Alifatisk 3y ago
  Is Xr0 the only ongoing project to provide Safe C?
• FrankWilhoit 3y ago
  This is one way to go; but the only "problem" with C is management's expectation that production software can be written by people who have only half learned the language, and that is a problem irrespective of which language we are talking about.
  • cultofmetatron 3y ago
    it takes literal years for someone to get to a point where they can ship proper c code and the process of getting good requires shipping c code when you don't know everything yet. having a system that automates and enforces years of collective knowledge on juniors is great and lets them contribute while they acquire experience.
  • stephencanon 3y ago
    There’s also engineers’ belief that they have learned the language despite only half-knowing it at best.
    • mtklein 3y ago
      I think this is actually one of the selling points of C over other languages. Certainly it's easy to fool yourself into thinking you know any language better than you do, but C genuinely is relatively tiny, and I think it's reasonable to expect to become familiar with almost everything in the language in a month or so of full-time work. After a decade of day job C++ coding, I'd not say the same for myself there. Rust and C++ lately have been particularly quickly moving targets to keep up with, where C is still pretty much the same as C99. The compilers are better, their warnings are better, sanitizer modes are incredible, but the things you type into your text editor to express your program structure are still pretty much the same thing.
      • int_19h 3y ago
        I doubt that a month of so of full work will get someone fully proficient on e.g. the finer details of integer promotions and how they can break things in non-obvious ways (think of situations such as combining signed and unsigned operands of different widths). The fundamental problem is that sane production code written in C will generally deliberately avoid some aspects of the language precisely because they are so footgun-prone, which means that if you learn solely by experience, you may never even become aware of the footgun behind the pattern.
• Animats 3y ago
  Nice. Are any of the many "safe versions of C" getting any traction? There have been so many. It's not a technical problem. It's a mindshare problem. The future in this area may be something that takes in existing C code and uses a LLM to recognize idioms and annotate. Without some automated way to convert legacy code, this isn't going to happen. (One big problem with converting to Rust is that Rust's data model is so far from C/C++ that you can't really convert much existing code. You have to rethink the design to fit the affine type model. That's hard.)
  • simonask 3y ago
    Rust's data model diverged from C++, but it's not very far from C. It's easy enough to write C-compatible structs and functions in Rust, as long as you don't need `Drop`. Even tagged unions (data carrying enums) are supported to some degree.
    • Animats 3y ago
      It's the lack of backlinks to parents that gets you. Rust can do hierarchies where an A owns a B which owns a C, but if you have a reference to C, you can't get back to A. (Yes, weak pointers, reference counts, unsafe hacks, etc. can work around that. But the language really doesn't like links to parents.) So there's no direct translation from a C++ object hierarchy to Rust structs.
  • littlestymaar 3y ago
    > (One big problem with converting to Rust is that Rust's data model is so far from C/C++ that you can't really convert much existing code. You have to rethink the design to fit the affine type model. That's hard.) True, but that's likely going to be the case as well to convert to any ”safe version of C” as well, because in the general case the safety of a C program is undecidable: to make it safe, you have to restrict it to a subset of behaviors that can be statically proven as safe, and the borrow checker and “Rust's data model” is just that.
  • pizlonator 3y ago
    I'm attempting something. https://www.youtube.com/watch?v=Gij9UQy_JEQ https://www.youtube.com/watch?v=Gij9UQy_JEQ https://github.com/pizlonator/llvm-project-deluge/blob/deluge/Manifesto.md https://github.com/pizlonator/llvm-project-deluge/blob/delug... Right now I'm ~90% through a major rewrite to use GC instead of isoheaps, because then I'll go from rewrite-a-bit (Fil-C previously required malloc calls to be annotated and for some unions to be changed) to rewrite-nothing (malloc will Just Work and so will unions). I hope there are others also trying various alternatives. It's too soon for most of these things to tell what traction they may or may not get.
• jnwatson 3y ago
  The problem with the safe C subsets is that it means you have to write new code. But if you have to write new code, why would you do it in C?
  • flohofwoe 3y ago
    Most of the proposals I've seen so far work via annotating existing code, not complete rewrites (e.g. here's one example from Apple: https://discourse.llvm.org/t/rfc-enforcing-bounds-safety-in-c-fbounds-safety/70854 https://discourse.llvm.org/t/rfc-enforcing-bounds-safety-in-...)
  • gpderetta 3y ago
    Annotating, possibly incrementally, existing code would be way easier than a rewrite. Safety annotations is the directions that C++ has been attempting without much success for a while though, so I'm not very optimistic. But I'm always happy to see another attempt.
  • graemep 3y ago
    A bit unfair. It verifies a subset of C because it is incomplete. It looks as though the idea is that you can annotate existing code, which is a lot easier than rewriting.
    • muldvarp 3y ago
      As someone who tried to get Frama-C working on existing code: No, annotating existing code is not much easier than rewriting it. In fact, to make these annotations practical, I had to rewrite parts of the code anyway.
    • KerrAvon 3y ago
      You have to understand the code at a level sufficient to make accurate annotations, which isn't that much easier. And you're not getting as much safety bang for your buck for the effort as you would in a rewrite in actually safe language.
      • 3y ago
• camel-cdr 3y ago
  C has a minimal, interpreted, safe, functional language embeded into it. You just have to execute it with cc -P -E, no need to run any fancy generated binary.
  • incanus77 3y ago
    If you're talking about GCC, I wonder if you can say more about this? I mean, I see the options, but I'm not entirely following. https://gcc.gnu.org/onlinedocs/gcc/Preprocessor-Options.html https://gcc.gnu.org/onlinedocs/gcc/Preprocessor-Options.html
    • moron4hire 3y ago
      It's a joke about coding in just the preprocessor
• woodruffw 3y ago
  Homepage seems to focus mostly on temporal memory safety; there isn't much said about spatial memory safety or memory-safe-but-unsound primitives, like type confusion. These should be table stakes when talking about "safe" languages (or subsets thereof); I hope these authors have or propose plans for these classes as well! (I agree with the more general critique here, that any adaptation invasive enough to provide these properties in C might as well be its own programming language.)
  • adamrezich 3y ago
    There is no universally-accepted definition for the term "safe" as it applies to programming languages.
    • gpderetta 3y ago
      While we can of course always bikeshed the minutiae, memory safety is a fairly well accepted and well defined term. And so are temporal and spatial safety (as subsets of memory safety). I would add that temporal safety is significantly harder than spatial safety (spatial safety is only hard in C if you do not want to break the ABI), so it is nice that this project is focusing on it.
    • tialaramex 3y ago
      True and yet useless. When "that's not safe" turns into a "discussion" about what safety means (e.g. at basically every C++ conference for over a year) what that signals is that you're much more interested in preserving the status quo than improving safety.
      • adamrezich 3y ago
        Alternatively, it signals that "safety" as a broad concept as it applies to programming languages, is pretty incoherent and ultimately useless. "Safe" and "safety" are very overloaded English words that come with a lot of baggage, and perhaps it would be prudent to stop using these broad, nonspecific terms for things like programming languages. "Memory safety" is a coherent, reasonably well-defined concept, and it's fine to talk about something like that. But what does a broadly, generically "safe" programming language even mean?
• steveklabnik 3y ago
  Posted last week: https://news.ycombinator.com/item?id=39858240 https://news.ycombinator.com/item?id=39858240
  • dang 3y ago
    That thread only spent 18 minutes on HN's front page, perhaps because of the baity title, so it's probably ok to have another go.
    • steveklabnik 3y ago
      For sure, not trying to say it shouldn’t be :) comments are way better this time around.
• naasking 3y ago
  They need a guide to compare it frama-c and other systems with annotations. Or at least compare what the objective ultimately will be, since this is still in its infancy.
  • muldvarp 3y ago
    Yeah, this doesn't really do anything for now. It currently doesn't even implement loops. I don't see why I would ever choose this over Frama-C which basically does the same (and is actually battle-tested). I just don't see a niche: - No full control over runtime needed: Java, C#, Python, ... - Full control over runtime and memory safety: Rust - Full control over runtime, memory safety and provable absence/presence of certain behaviors (i.e. aerospace, nuclear reactors, ...): Frama-C, CBMC, Astree, ... Where does Xr0 fit in and how does it differ from existing technology? The fact that they don't even mention any of those tools makes me believe that they are either not aware of them or that they are aware and the difference between this and Frama-C is just syntactic. Not a good look either way.
    • akiarie 3y ago
      Since we are not academics, I don't see why we're under obligation to do a comprehensive literature review, especially early on. We aren't claiming to have invented these techniques. It should be obvious that Xr0 involves very little in the way of new ideas. Our primary reference has been the work of Dijkstra. What is significant about Xr0 is how it applies these old ideas. Xr0 is designed for programmers rather than mathematicians, so to us syntax matters a great, great deal.
      • muldvarp 3y ago
        > Since we are not academics, I don't see why we're under obligation to do a comprehensive literature review, especially early on. I don't think you're under any obligation, I just think that not discussing prior art is a bad look. > What is significant about Xr0 is how it applies these old ideas. I don't see anything new about the application of these well-known ideas either. Especially nothing that could explain why Xr0 would be widely used, while Frama-C is extremely niche. > Xr0 is designed for programmers rather than mathematicians, so to us syntax matters a great, great deal. Proving (the correctness of code) is an inherently mathematical task. So if by "mathematician" you mean someone who does mathematics, then all of your users will be mathematicians.
• nextaccountic 3y ago
  What about data races? (I can't find anything about it in this page) Avoiding UB in single threaded programs is the easy part. It's harder for a low level language like C, but not too hard. But avoiding UB in multithreaded programs is very very hard. Many "safe" managed languages have UB when you misuse synchronization mechanisms, like Go. Some languages Java and OCaml manage to avoid UB when you have data races. They do so by disallowing some compiler optimizations. OCaml is the better one in this regard (see the paper "bounding data races in time and space")
  • betz47 3y ago
    Xr0 is currently targeting the c89 spec and working up from there, thread safety is something that we would address in C11 (See a previous discussion here https://news.ycombinator.com/item?id=39858240#39858813 https://news.ycombinator.com/item?id=39858240#39858813).
    • nextaccountic 3y ago
      That's exciting! Is there any proposal or rough ideas or musings or anything that might suggest how Xr0 could possibly guarantee data race freedom? Would it be something like Rust's Send & Sync traits? Or something else entirely?
• deleted 3y ago
  [deleted]
• Uptrenda 3y ago
  [flagged]
  • int_19h 3y ago
    Quite frankly, the "leave me alone, I know what I'm doing!!1!" people have had over 50 years now to prove that they can consistently write safe code as a group. All evidence so far points to the contrary. FWIW I don't think Rust is the answer to this, either. Most software just needs to be written on an even higher abstraction level, with copious redundant safety nets embedded on all levels, performance be damned. It appears that that's the only way we as an industry can reach acceptable quality of software with the average developer that we actually have (as opposed to the hypothetical Zen master).
  • steveklabnik 3y ago
    What makes you think a Rust person made this? I don’t really see any evidence of that.
  • wredcoll 3y ago
    Thank you for taking the time to bring the average level of discourse around here down yet another level.
    • tgv 3y ago
      It is the best written reply in this thread. The style is great, up until "ur azz". I'd have appreciated a less hackneyed metaphor, but I can understand the author wanted to finish the lament. What does surprise is me why someone is so strongly opposed to something that is optional, is a support, and doesn't even get in the way of laying bare the algorithm. It's an annotation to the function declaration, not unlike a return type. Perhaps it's the verbosity?