LINUX.ORG.RU

Вышел CompCert 2.0

 


3

3

CompCert — это компилятор языка программирования Си (ANSI C с незначительными ограничениями) для платформ PowerPC, ARM и IA32, предназначенный для сборки программ с повышенными требованиями надежности и дополняющий формальные методы проверки (статический анализ, проверка на модели и т.п.) на уровне исходного кода.

Некоторые изменения:

  • поддержка типов long long и unsigned long long;
  • предварительная поддержка отладочной информации;
  • агрессивная стратегия исключения дублирующегося кода;
  • уменьшено потребление памяти при компиляции;
  • исправлены некоторые ошибки.

Исходные коды компилятора распространяются на условиях лицензии «INRIA Non-Commercial License Agreement».

>>> Подробности

★★★★★

Проверено: tazhate ()

Что это вообще за хрень? Статический анализ C и clang отлично делает, если кому-то надо лучше — пожалуйста, шлите им патчи. Thread sanitizer и memory sanitizer теперь и в clang, и в GCC есть.

А уж «надёжный» компилятор без отладочной информации — это вообще чепуха полная. Ещё и лицензия проприетарная, вкупе с враньём про надёжность.

quiet_readonly ★★★★ ()
Последнее исправление: quiet_readonly (всего исправлений: 1)
Ответ на: комментарий от ymn

man формальная верификация

Т.е компилятор не поддерживает отладочную информацию, но при этом будет верифицирован как корректный компилятор C? Как будет верифицирован сам стандарт C? Стандартная библиотека? Нафига нужен компилятор без расширений?

В общем все сказки про верификацию этого убожества — это очевидное маркетинговое враньё.

quiet_readonly ★★★★ ()
Последнее исправление: quiet_readonly (всего исправлений: 1)

Интересная штука - впервые увидел практическое применение Coq и Caml, да ещё и в одном проекте.

Ух, да там и Xavier Leroy приложился...

unsigned ★★★ ()
Последнее исправление: unsigned (всего исправлений: 1)
Ответ на: комментарий от quiet_readonly

это очевидное _маркетинговое_ враньё

«_INRIA_ Non-Commercial License Agreement».

Ага у них лишь маркетинг в голове, будут продвигать также как и «coq enterprise edition» и «ocaml corporate version».

anonymous ()

мдяяяя. лучше бы они просто проверятор исходного кода сделали. а компиляторы уже есть, в количестве как минимум аж четырёх штук - gcc, clang, pcc, tcc. теперь пять.

u283 ()

ymn, допиши, что компилятор сам по себе верифицирован, а то непонятно. А это - «дополняющий формальные методы проверки на уровне исходного кода» вообще туманно.

И ещё, допускается свободное использование в обучении и исследованиях. А половина кода dual-licensed под GPL2+.

unsigned ★★★ ()
Ответ на: комментарий от u283

они сделали, в отличии от тебя.

http://frama-c.com/

compsert не смотрел, но думается мне это связанные проекты.

anonymous ()
Ответ на: комментарий от quiet_readonly

ты, похоже, идиот. Тебе никогда не хотелось биться головой о стол из-за того, что какой-нибудь очередной гнутый gcc вместо корректного бинарного кода выдаёт падающее говно? Здесь на ЛОРе была как минимум одна новость о дыре в лялексовом ведре, порождённой именно кривостью gcc, который любит выкинуть «лишние» инструкции ради оптимизации. И это далеко не единичный случай - на отличных от x86 платформах gcc очень часто выдаёт полную хрень.

anonymous ()
Ответ на: комментарий от unsigned

Часто применение новых методов вовсе не связано с необходимостью. То есть, ту же задачу можно решить проверенными старыми надёжными разработками. Но чтобы маркетологам было что говорить на презентации, вводят новинку. Сколько ни пытаюсь понять, где же кок применить можно - ничего реально необходимого, невозможного сделать традиционными способами, - ничего придумать не могу. Скептицизм quiet_readonly разделяю чуть менее чем полностью.

Stalin ★★★★★ ()
Ответ на: комментарий от quiet_readonly

Как будет верифицирован сам стандарт C? Стандартная библиотека?

Исходник на си «elabor»-ируется в исходник Clight, который представляет собой «правильное» подмножество си с уже точно определёнными синтаксисом и семантикой, он уже и верифицируется дальше. То есть не весь сишный код заведётся (duff's device, например — нет).

Ещё на тему «как» — у них на сайте, http://compcert.inria.fr/publi.html.

Ну и Clight это не первая формализация си:

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.6755

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.9279

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.124.5712

Нафига нужен компилятор без расширений?

«Part of Leroy’s achievement is that he makes it look like it's not so difficult after all: now that he's found the right architecture for building verified compilers, everyone will know how to do it.» (с) Andrew Appel.

То есть чтобы показать как надо делать такого рода вещь — если это понятно, то дальше можно уже писать и «промышленный» верифицируемый компилятор с расширениями, а gcc и clang могут спать спокойно — маркетологи из INRIA не пройдутъ :)

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

ты, похоже, идиот

Да как обычно: скорее всего провокация, чтобы объяснили (в порыве праведного гнев) что к чем, получить больше информации.

Но перебор, молча слиться не смог - пошел неадекват.

anonymous ()
Ответ на: комментарий от anonymous

любит выкинуть «лишние» инструкции ради оптимизации

man volatile man barriers

Какие линуксоиды такой и линукс.

anonymous ()
Ответ на: комментарий от anonymous

man volatile man barriers

что volatile и barriers, когда целый вызов memset() выкидывается? Ты предлагаешь на каждый указатель ставить volatile?

anonymous ()
Ответ на: комментарий от Stalin

Часто применение новых методов вовсе не связано с необходимостью

Есть случаи, когда формальное доказательство корректности необходимо, юридически и/или фактически. Их мало, но это и не продукт для массового применения.

ту же задачу можно решить проверенными старыми надёжными разработками

Что ты считаешь надежной разработкой - gcc, clang, ...? Готов взять на себя административную/уголовную ответственность за их выхлоп, который пойдет на критически важную железку?

Но чтобы маркетологам было что говорить на презентации, вводят новинку

Это, похоже, академический проект. Да и вообще, кому нужна верификация - те и так об этом знают, а остальных никто уговаривать не будет.

unsigned ★★★ ()
Ответ на: комментарий от I-Love-Microsoft

да не, за границы массива запросто.

просто верифицированный компилятор как я понимаю гарантирует что он накомпиляет именно то что ты написал на си, а не какой то левый код (из-за ошибки в логике компилятора).

AndreyKl ★★★★★ ()
Ответ на: комментарий от I-Love-Microsoft

Я правильно понимаю что за границы массива в коде на таком компиляторе уже не выедешь?

Это невозможно статически проверить, кроме простейших случаев.

unsigned ★★★ ()
Ответ на: комментарий от unsigned

Готов взять на себя административную/уголовную ответственность за их выхлоп, который пойдет на критически важную железку?

Я не поняла, а кто даст гарантию что не будет неправильно инциализирован указатель? Это какой-то маркетинговый пердеж про супернадежные компиляторы. Тут катят другие подходы, для суперважных железок С и С++ вообще запрещено использовать.

anonymous ()
Ответ на: комментарий от anonymous

Вот я читаю «для сборки программ с повышенными требованиями надежности», а теперь я хочу спросить как в убогом от рождения С, эти люди мне обеспечат надежность?

anonymous ()
Ответ на: комментарий от unsigned

Это невозможно статически проверить, кроме простейших случаев.

Это возможно — индекс массива должен быть не типа size_t, а типа Σ (x : size_t) x < размер_массива.

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

суперважных железок С и С++ вообще запрещено использовать.

откуда дровишки? Минобороны США для суперважных железок вообще котирует вообще только три языка: C, C++ (с большими ограничениями) и Ada.

anonymous ()
Ответ на: комментарий от quasimoto

Это возможно — индекс массива должен быть не типа size_t, а типа Σ (x : size_t) x < размер_массива.

Поздравляю, ты изобрёл зависимые типы. Только в C их нет.

anonymous ()
Ответ на: комментарий от anonymous

Ты предлагаешь на каждый указатель ставить volatile?

Volatile как раз не следует применять. Есть же барьеры.

Deleted ()
Ответ на: комментарий от Deleted

Volatile как раз не следует применять. Есть же барьеры.

как помогут барьеры, если компилятор УБИРАЕТ вызов функции?

http://gcc.gnu.org/bugzilla/show_bug.cgi?id=8537

вот тебе пример. И такое поведение встречается до сих пор (на дворе 2013 год, да).

anonymous ()
Ответ на: комментарий от anonymous

Проснись уже. Для мишн-критикал апликух сто лет как уже используется ява и ничего кроме ява, про С все забыли как страшный сон.

anonymous ()
Ответ на: комментарий от anonymous

Сам дурак.

The Java coding standard in its entirety has, in collaboration with Semmle, been implemented in Semmle’s static code analyzer, and is currently being tested on JPL internal projects, including the MSL telemetry and command ground software.

Benefits:

Risk reduction on mission-critical software Rapid development of custom analyses

Klaus Havelund and Gerard J. Holzmann, leaders of NASA JPL's Laboratory for Reliable Software (LaRS).

anonymous ()
Ответ на: комментарий от anonymous

Ну что, обрыган, будешь еще тут кукарекать про JPL?

anonymous ()

Есть ли случаи дружбы этого компилятора с Objective-C ?

Infra_HDC ★★★★★ ()
Ответ на: комментарий от unsigned

А для C++ - возможно?

Либо type level извращения на шаблонах (http://pwparchive.wordpress.com/2012/03/29/dependent-typing-in-c/). Либо enum-ы:

template<size_t n>
struct Ix;

template<>
struct Ix<2> {
    enum class EnumType : size_t {
        zero, one
    };
};

template<>
struct Ix<3> {
    enum class EnumType : size_t {
        zero, one, two
    };
};

template<size_t n, typename A>
A get(std::array<A, n> xs, typename Ix<n>::EnumType i)
{
    return xs[static_cast<size_t>(i)];
}

    std::array<int, 3> xs = {{ 1, 2, 3 }};
    printf("%d\n", get(xs, Ix<3>::EnumType::zero));

связывать предикатные типы с обычными числами — как-то не представляю. Последние, по сути, заставляют всюду в коде доказывать что числа лежат в нужных границах, хотя бы и в виде обычных if-guards — всё равно получаются статические гарантии.

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

Поздравляю, ты изобрёл зависимые типы.

С чего это мне их изобретать? https://en.wikipedia.org/wiki/Intuitionistic_type_theory#.CE.A3-types

Тут — изоморфно fin типам и правильным enum-ам.

Только в C их нет.

Ближайший аналог именно такого типа — enum-ы, но они в си сломанные.

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

как помогут барьеры, если компилятор УБИРАЕТ вызов функции?

А нахрена тупить и писать такой код? Там достаточно прочитать память после записи — и «баг» исчезнет.

В общем GCC с -O0 будет делать то же самое, что и это маркетинговое посмешище.

quiet_readonly ★★★★ ()
Ответ на: комментарий от quiet_readonly

А нахрена тупить и писать такой код?

это ты здесь тупишь, болезный. Компилятор, изменяющий семантику кода должен гнить в отстойнике вместе с его авторами.

anonymous ()
Ответ на: комментарий от anonymous

это ты здесь тупишь, болезный. Компилятор, изменяющий семантику кода должен гнить в отстойнике вместе с его авторами.

GCC -O0 не изменяет. Любой оптимизирующий изменяет, если под семантикой кто-то понимает ещё и состояние регистров и памяти.

Но если программист заботится о содержимом памяти и регистра и при этом делает это без учёта особенностей оптимизирующего компилятора, то он мудак.

quiet_readonly ★★★★ ()
Ответ на: комментарий от quiet_readonly

модератор грохнул мой комментарий. Пусть сам тебе теперь отвечает, хуле.

anonymous ()
Ответ на: комментарий от unsigned

Gcc - основной компилятор для например Mac OS X, Linux, да и для других операционных систем так же. В Мас OS X конечно и LLVM есть, но он тоже родом из gcc.

Так что нелепо критиковать gcc на основе качества генерируемого кода, оно на уровне и проверено временем и используется сообществом.

anonymous ()
Ответ на: комментарий от anonymous

Филипп Киркоров - ...

Аргумент к популярности можешь засунуть себе глубоко в задницу. Твоё сообщество использует его дай бог на полутора архитектурах с дефолтными опциями. Стоит отойти от этого, и сразу лезут килотонны багов.

В OS X используется старая ветка gcc с кучей собственных патчей, потому что разработчики из GNU не спешат исправлять многие ошибки по причине собственной импотенции.

LLVM - совершенно сторонний, не имеющий никакого отношения к GCC проект (подумай головой, дубина, GCC лицензирован под GPL, а LLVM - нет).

anonymous ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.