Slashdot Mirror
C with Safety - Cyclone
Paul Smith writes: "New Scientist is carrying a story about a redesigned version of the programming language C called Cyclone from AT&T labs. "The Cyclone compiler identifies segments of code that could eventually cause such problems using a "type-checking engine". This does not just look for specific strings of code, but analyses the code's purpose and singles out conflicts known to be potentially dangerous.""
Not a flame, but more "modern" languages such as Java and C# have constructs explicitly built to avoid the buffer overflow/pointer gone insane problems.
For the rest of the world, secure C programing is far from a secret.
Easy does it!
This comment has been submitted already, 276865 hours , 59 minutes ago. No need to try again.
(right on the web page detailing the language)
A lot of the static checking made possible by Cyclone can be done for ordinary C with lclint, which lets you add annotations to C source code to express things like 'this pointer may not be null', 'this is the only pointer to the object' and so on. You write these assertions as special comments, for example /*@notnull@*/. These are checked by lclint but (of course) ignored by a C compiler so you compile as normal.
(If you weaken the checking done, lclint can also act as a traditional 'lint' program.)
Also C++ provides a lot of the Cyclone features, not all of them, but it certainly has a stronger type system than C. I'd like to see something which combines all three: an lclint-type program that lets you annotate C++ code to provide the extra checks that Cyclone (and lclint) have over C++.
-- Ed Avis ed@membled.com
Seems to me PC-LINT gives you the same contextual checking... but I could be mistaken.
you're not up-to-date on some bullets
the 1.4 jdk (currently in beta) has pattern matching
parametric polymorphism (iow - templates) are in development and being called generics
The One Rule Of Chess You'll Ever Need: Don't play someone who carries a kit in their bookbag.
lint - is name of it. And it was made 20 years ago.
p.
Ever had an agressive optimizer break code, such that you had to use a lower optimization setting? This can be a symptom of weakness in the compiler's ability to statically analyze the program. Not just a garden variety "bug", but rather the optimization is correct only for a subset of valid input source code! I.e. it can be difficult to impossible to prove that a given optimization is safe, aka "semantics preserving".
Many modern PL researcher/designers thus aim to give compiler writers a head start by ensuring that the language design permits increasingly powerful forms of static program analysis. Functional language work in particular has focused heavily on utilizing language and type system design to enable more powerful analysis support. (cf. the various published papers on the Haskell and OCaml languages as a starting point).
REGULAR EXPRESSIONS ARE NOT PATTERN MATCHING (in this context)
Please read what pattern matching means when Safe-C (and ML and Prolog and Erlang and...) says "pattern matching" before you post your irrelevant link anymore.
Back in grad school, I used to read comp.theory, and at least once a month, we'd have some jerk post to the newsgroup "NP solved!", followed by some stupid, exponential time algorithm for 3-SAT or something. Invariably, the poster would spend thousands of lines defending his supreme genius in being the person who solved an NP complete problem!
NP complete does not mean unsolvable. It means slow.
Roughly speaking, NP problems are problems for which their is no non-exponential time solution known, but for which solutions can be tested for correctness in polynomial time. (To translate, exponential time means that the time to compute the solution for a problem of size n is bounded by x^n for some n. Polynomial time means that the time for a problem of size n can be bounded by some polynomial of n.)
The travelling salesman is a classic example of an NP problem. Given a set of cities, and the distance between any two cities, compute the shortest route that visits each city once. It's a trivial problem, but as far as anyone knows, it's not possible to write a program that quickly determines the correct shortest route in every case.
NP complete problems are problems which have the fascinating problem that *if* you found a polynomial time solution for that problem, then you would have found a polynomial time solution for all NP problems.
The travelling salesman is, if I recall correctly, slightly *worse* than NP complete. Again, if I recall correctly, if you have a P-time solution to the TSP, then you provably have a P-time solution to any NP-complete problem; but if you have a P-time solution for an NP-complete problem, that doesn't mean that you have a P-time solution to the TSP. The proof is actually quite interesting, so go get an algorithm textbook, and read it. I'd suggest the Corman, Leiserson and Rivest text, which is my personal favorite.
There are perfect, well known solutions for all of the classic NP complete problems. They're just exponential time. (For instance, for the travelling salesman: enumerate all possible routes; compute the length of each route; and pick the shortest one.)
Cyclone is a remarkable achievement, given they
started with C...
MISRA-C is also a good effort, although somewhat
built on sand.
The safety-critical community over here in Europe,
and also a few projects in the USA use SPARK
though, which is a high-integrity, annotated
subset of Ada. It's static analysis tool
is really remarkable - anyone for static proof
of exception freedom? (e.g. static proof of
no buffer overflow for all input data)
Eiffel is also very good from a high-integrity
point of view, and well worth a look. It amazes
me how much effort goes into researching static
analysis of langauges that are simple not designed
for that purpose at all...ah well...
- Rod Chapman
Be careful pointing the finger about ignorant mistakes.
TSP cannot be worse than NP-complete, because it is obviously in NP. Phrased as a decision problem (is there a Hamilton path through this graph shorter than length y?) it is trivial to verify a solution in polynomial time. If you can verify in P, you can solve in NP.
Note that rephrasing as a decision problem doesn't change the order much, because you can just do a binary search with O(log N) steps where each is a decision subproblem. Also note that transforming it into a decision problem is *necessary* to discuss its NP-completeness, because the very concept is only defined for decision problems.
Java: the COBOL of the new millenium.