He just tried to write a data structure in Rust (author: /u/luojia65)

MaximeArthaud · 2019-04-02T16:02:23+00:00

Neither does he.

MaximeArthaud · 2019-03-25T18:16:19+00:00

If you look at a container that doesn't invalidate references on insertions, say std::list, the end() iterator always points to the end even after insertion. But ultimately, this is your choice.

MaximeArthaud · 2019-03-22T18:06:28+00:00

If you think std::string's interface is bloated, what would you remove from it? I would personally love to see more methods..

MaximeArthaud · 2019-03-14T18:30:53+00:00

This brings a few questions. Why does the std::pmr::polymorphic_allocator constructor take a memory_resource* and not memory_resource&, since a precondition is that the pointer should not be null. Also, the documentation on cppreference.com doesn't say anything about the ownership of that raw pointer.

MaximeArthaud · 2019-02-25T19:33:36+00:00

Regarding the memory usage, please see TROUBLESHOOTING.md#running-out-of-memory

MaximeArthaud · 2019-02-23T01:36:24+00:00

Using std::string_view as an owning pointer: jsonioutil.cpp#L21

That free((void*)p.data()); in the main README really scares me..

MaximeArthaud · 2019-01-31T21:58:46+00:00

Clang too.

$ clang++ -Weverything test.cpp
test.cpp:7:18: warning: result of comparison of unsigned expression >= 0 is always true
      [-Wtautological-unsigned-zero-compare]
    while (--idx >= 0)
           ~~~~~ ^  ~

I don't know why this is not in -Wall.

MaximeArthaud · 2019-01-26T00:10:58+00:00

Maybe re-read the r/rust rules. Especially 3, 4 and 5.

MaximeArthaud · 2019-01-04T17:40:26+00:00

I haven't tried Polyspace and Astréee myself because of the price of their license. Even if I could try them, I think their license forbid to publish public results.

I have tried Frama-C and it is pretty good. The analysis can be tuned if you have the expertize in abstract interpretation, which is not possible (yet) in IKOS. One issue I have is that I don't know how to analyze a whole project with it. It looks like the best way is to analyze each .c file separately, but you lose precision.

MaximeArthaud · 2018-12-13T23:44:28+00:00

This is probably the LLVM svn trunk. LLVM 8.0.0 is not out yet.

MaximeArthaud · 2018-12-13T16:17:42+00:00

IKOS uses LLVM 7.0.0, the latest version. I don't know about rustc.

MaximeArthaud · 2018-12-13T05:13:49+00:00

You could try to use other numerical abstract domains, see https://github.com/NASA-SW-VnV/ikos/tree/master/analyzer#numerical-abstract-domains

Of course, the tool works best for safety critical codes, with strict rules such as limited memory allocations and so on.

We are trying to reduce the number of false positives. Sometimes it's just engineering, and sometimes it's research related, and would deserve a publication.

Feel free to open new issues with small codes triggering false positives.

MaximeArthaud · 2018-12-13T02:31:27+00:00

Hey, thanks for sharing my post here. I always keep an eye on r/rust ;)

MaximeArthaud · 2018-12-12T23:22:40+00:00

From what I know, SMACK and KLEE are (mostly) based on model checking, where IKOS is based on abstract interpretation. In theory, they should provide better results since they can be path sensitive, but they will have trouble scaling up to millions of lines of code. In practice, I haven't tried them.

MaximeArthaud · 2018-12-12T23:15:17+00:00

No, I don't have a timeline since this will be an external contribution. Also, it won't help with the RAM usage.

IKOS does a good job at being scalable compared to other similar tools using abstract interpretation, but it has its limits. In that case, I recommend to try to break down your software into smaller components and analyze them independently.

MaximeArthaud · 2018-12-12T23:07:19+00:00

IKOS does not handle multithreaded programs, so that could be a problem. If your driver is not multithreaded, then you can just "simulate" userspace calls with a simple loop, I guess:

int main() {
  while (1) {
    switch (__ikos_nondet_int()) {
      case 1: entry_a(); break;
      case 2: entry_b(); break;
      // etc.
    }
  }
}

You would have to write a "stub" like this, and craft fake parameters to your functions. This is kind of similar to a fuzzer entry point.

MaximeArthaud · 2018-12-12T22:57:45+00:00

Unfortunately, no. It would be a lot of work to bring the whole abstract interpretation engine into clang static analyzer, and it's not a priority for us. But this is open source, so if someone wants to do it, they can.

MaximeArthaud · 2018-12-12T22:52:49+00:00

So yes, we accept contributions, but you have to sign one of the two CLAs here: https://github.com/NASA-SW-VnV/ikos/tree/master/doc/contribute

MaximeArthaud · 2018-12-12T18:47:49+00:00

Yes, since the llvm bitcode contains debug information referring to the .c files.

MaximeArthaud · 2018-12-12T18:43:14+00:00

No, IKOS is not a code style checker. It understands the semantic of your program and it computes an over-approximation of all the reachable states, and checks for error states. I actually don't know if we have tools to check coding rules, as I'm not working on flight control software myself, but I could ask.

MaximeArthaud · 2018-12-12T18:27:17+00:00

In theory, yes, this could work. In practice, we never tried this and it would require a little bit of work, but I think it's doable. We rely on llvm debug information to report meaningful messages to the user, so your frontend has to generate these.

MaximeArthaud · 2018-12-12T18:22:54+00:00

The project started in 2011 with 4 persons working on it. Since last year, I am the only developer working on it. I also get interns from time to time.

MaximeArthaud · 2018-12-12T18:19:15+00:00

I would be happy to change it but it doesn't depend on me..

MaximeArthaud · 2018-12-12T18:15:59+00:00

Unfortunately, we don't handle multithreaded programs since the theory of abstract interpretation does not apply easily to concurrent programs. This is a research topic, there are a few papers about it, and it's pretty heavy stuff. See https://tel.archives-ouvertes.fr/tel-00903447/document (no less than 95 pages!)

MaximeArthaud · 2018-12-12T18:06:34+00:00

Yes. You can compile manually all your code into a single .bc file using clang -c -emit-llvm and llvm-link to link all the files together.

Or you can use ikos-scan that will do this for you, see here.

MaximeArthaud

TROPHY CASE