Вышел CompCert 2.0

http://harmful.cat-v.org/software/GCC — добавлю ссылку, пожалуй.

-O0 И ВСЕ ОК

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

От вас ничего не скроешь. На то вы и генерал!(с)

Князь? Не узнаю вас в гриме.

1) Какие ещё полторы архитектуры? GCC есть на всех архитектурах (или почти на всех), если о процессорных идёт речь. Если об ОС - то gcc есть на всех плоатформах, а компилятором по-умолчанию является на Linux, OS X , *BSD

2) Про LLVM& http://en.wikipedia.org/wiki/LLVM - LLVM was originally written to be a replacement for the existing code generator in the GCC stack,[14] and many of the GCC front ends have been modified to work with it. LLVM currently supports compiling of Ada, C, C++, D, Fortran, and Objective-C, using various front ends, some derived from version 4.0.1 and 4.2 of the GNU Compiler Collection (GCC).

Комментарии излишни, это не новый компилятор.

3) Про баги в gcc - голословно, видать вообще не в курсе. GCC - один из самых базбаговых компиляторов с лёгкостью их поиска и исправления. Если что и есть в gcc - это неоптимальности, но это вне рамок обсуждения тут темы компилятора, про который ничего не известно.

-O0 И ВСЕ ОК

наивный... Ты просто не видел, что gcc выдаёт для mips для чисел с плавающей точкой. Даже с -O0, да.

Про баги в gcc - голословно, видать вообще не в курсе

видать ты давно в их багзиллу не смотрел.

Главное - выдаётся корректный код. А то, что нет оптимизаций - так это не главное. На то есть родные компиляторы, которые не переносимы на другие архитектуры. Не наод всё мешать в одну кучу - и кроссплатформность и максимум оптимизаций.

давно в багзиллу не смотрел

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

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

Да, на дворе 2013-й год, а компиляторы так и не научились читать мысли программистов и при оптимизации выкидывают операции записи в области памяти, которые потом всë равно читать никто не будет. И да, для чистки памяти есть спец. функции наподобие OPENSSL_cleanse которые заполняют указанную область памяти [псевдо]случайным мусором, а не просто нулями, и не выкидываются оптимизатором, т.к. он тупо не знает, что эта функция делает.

Ещё слегка поправленный вариант для тех же статических std::array:

#include <array>
#include <functional>
#include <iostream>

#include <boost/optional/optional.hpp>

template<size_t n> struct fin_s;
template<> struct fin_s<1> { enum enum_type : size_t { _0 }; };
template<> struct fin_s<2> { enum enum_type : size_t { _0, _1 }; };
template<> struct fin_s<3> { enum enum_type : size_t { _0, _1, _2 }; };
// ...

template <size_t n> using fin = typename fin_s<n>::enum_type;

template<size_t n, typename T>
T get(std::array<T, n> const& xs, fin<n> i)
{
    return xs[static_cast<size_t>(i)];
}

template <size_t n>
boost::optional<fin<n>> to_fin(size_t i)
{
    return i < n ? boost::optional<fin<n>>(static_cast<fin<n>>(i)) : boost::optional<fin<n>>();
}

// `optional' eliminator
template <typename A, typename T>
A choose(boost::optional<T> const& x, std::function<A()> f, std::function<A(T)> g)
{
    return x ? g(*x) : f();
}

int main()
{
    std::array<int, 3> xs = {{ 1, 2, 3 }};

    std::cout << "last is " << get(xs, fin<3>::_2) << std::endl;

    size_t i {};
    std::cin >> i;

    choose<void, fin<3>>(
        to_fin<3>(i),
        []() { std::cout << "bad index" << std::endl; },
        [&](fin<3> ix) {
            std::cout << "it is " << get(xs, ix) << std::endl;
        }
    );

}

GCC - один из самых базбаговых компиляторов с лёгкостью их поиска и исправления.

Докажи. Для CompCert доказано, что в нем нет багов. А вот поставил бы ты свою почку на безбаговость gcc?

Какой ужас, спасибо.

А если так:

#include <iostream>
#include <stddef.h>
 
const int MAX = 3;
 
template <size_t i> struct Int;
template <> struct Int<0> { enum Val { val = 0 }; };
template <> struct Int<MAX> {};
template <size_t i> struct Int { enum Val { val = Int<i - 1>::val + 1 }; };
 
int main()
{
        Int<N> i;
        std::cout << i.val << std::endl;
} 

$ g++ -DN=2 int.cpp && ./a.out
2
$ g++ -DN=3 int.cpp && ./a.out
int.cpp: In function `int main()':
int.cpp:14: `struct Int<3>' has no member named `val'
$

Вот только не могу никак MAX параметризовать.

Докажи. Для CompCert доказано, что в нем нет багов.

Что-то я не увидел, что в compcert нет багов. Посмотрел лог изменений - всё как у людей и баг-репорты есть и т.п. - http://compcert.inria.fr/release/Changelog

Вы путаете средства верификации программ с безбаговостью программы, то есть не разобрались в теме.

Из описания CompCert - компилятор предоставляет средства формальной верификации генерируемого кода исходному тексту программы. («The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to source programs.»)

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

А вот поставил бы ты свою почку на безбаговость gcc?

Это вообще странное заявление. Не собираюсь свои органы ставить куда бы то ни было и вам не советую.

Насколько я ещё помню - тот же gcc встроен в ОС МСВС, которая вполне себе сертифицирована и допущена до использования для решения некоторых критических задач в рамках программно-аппаратных комплексов - где верифицируется и архитектура и конкретные версии ПО с доработками, то есть на этих платформах gcc генерирует корректный код.

А если так

Так ты написал функцию id : fin<3> -> fin<3> в compile time, а нам надо сам этот тип для рантайма — населить fin<n> числами от 0 до n - 1:

// fin<3> -- тип из, ровно, 0, 1 и 2.
fin<3> x = 0;
fin<3> x = 1;
fin<3> x = 2;
// fin<3> x = 3; <- error

с кучей enum-ов под каждый n получается

fin<3> x = fin<3>::_0;
fin<3> x = fin<3>::_1;
fin<3> x = fin<3>::_2;
// fin<3> x = fin<3>::_3; <- error

причём n из fin<n> — в compile time, а вот значения типа fin<n> — в runtime, все меньше n, так что можно написать функции optional<fin<n>> to_fin(size_t) и size_t from_fin(fin<n>) и использовать такие ограниченные индексы в рантайме для безопасной индексации к std::array как T get(std::array<T, n> const& xs, fin<n> i) (видим, что i < n на уровне сигнатуры). optional нужен, choose — тоже, это типа «разыменование указателей done right» (eliminator для option/maybe, вообще, тип безопасно можно использовать только с помощью introduction (конструкторы), elimination (визиторы общего вида) и производных тотальных функций, всё остальное частичное и в обход introduction и elimination вроде разыменования указателя или get для optional в основе не безопасно и должно быть просто приватным / проверенным / на свой страх и риск, если интерфейс делается заведомо сильно типобезопасным), то есть это решение вопроса «как система типов будет угадывать, что сырые числа будут лежать в нужных границах во время выполнения?» — ничем не отличается от вопроса «как parse_integer будет угадывать, что строка будет валидным числом?», с помощью optional — если нет частичных функций / обхода правил типизации, то тут проблем не может быть в принципе.

Ещё такой fin можно сделать как рекурсивный

template<size_t n> struct fin_r { virtual size_t value() const = 0; };
template<size_t n> struct z : fin_r<n> { size_t value() const { return 0; } };
template<size_t n> struct s : fin_r<n> {
    fin_r<n - 1> const& prev;
    s(fin_r<n - 1> const& prev_) : prev(prev_) {}
    size_t value() const { return 1 + prev.value(); }
};

но

fin_r<3> const& x = z<3>{};
fin_r<3> const& x = s<3>(z<2>{});
fin_r<3> const& x = s<3>(s<2>(z<1>{}));

явно не удобно, плюс оно тормозит.

Частичной специализацией:

#include <iostream>
#include <stddef.h>

template <size_t n, size_t i> struct FinId;
template <size_t n> struct FinId<n, 0> { enum { val = 0 }; };
template <size_t n> struct FinId<n, n> {};
template <size_t n, size_t i> struct FinId { enum { val = FinId<n, i - 1>::val + 1 }; };

int main()
{
    FinId<N, I> x;
    std::cout << x.val << std::endl;
}

Что мы сделали? Калькулятор id на definaх :)

Такая техника нужна для type level значений и функций, тогда как искомый fin — обычный тип. Fin уровнем выше в type level так вообще не сделать, у С++, как и у Haskell, уровень значений статически типизирован типами, а вот уровень типов динамической — у всего один kind — typename в C++ и * в Haskell (хотя в GHC движутся в сторону усложнения kind-ов). Про типы kind-ов (sort-ы) и дальше вверх по иерархии тут вообще речи не может идти.

как и у Haskell

Хотя там есть * -> * и т.п., так что уже немного типизирован — можно писать то что в C++ нельзя писать как

template <function2<typename(typename)> F, typename T>
foo(F<T> x);

foo<std::list, int>(...);

Вы путаете средства верификации программ с безбаговостью программы, то есть не разобрались в теме.

В CompCert доказано, что ни одно из преобразований не вносит новых багов - то есть, что семантика скомпилированного кода тождественна исходной семантике.

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

Идиот. Редкостный. При чем тут верификация? Корректность преобразований ДОКАЗАНА. Строго.

Корректность преобразований ДОКАЗАНА. Строго.

Если ошибка в *исходном* коде (чуть менее, чем все встречающиеся баги) или вообще железе, то хоть обпреобразуйся, но результатом работы программы будет не то, что надо. Не стОит дрочить на формальную корректность компилятора, список критериев правильности работы программы им не ограничивается.

Ты быдло. Ни о какой корректности самой программы вообще речи быть не может, если компилятор некорректен.

А железо, между прочим, тоже формально верифицируют.

Ох, а идея статической формальной верификации программ-то ещё не умерла. Сколько ж раз нам этой идеей в университете мозг промывали. За 6 лет выслушал 4 или 5 курсов одного и того же, но немного отличающихся - после этого от одного только выражения «тройка Хоара» начинает тошнить. Но вообще ребята молодцы, успеха им.

Ты быдло.

О, илитная гопота в треде про компилятор. Okay.

Ты быдло. Ни о какой корректности самой программы вообще речи быть не может, если компилятор некорректен.

Какие мы вежливые. А какие критерии корректности компилятора? Компилятор всегда корректен. Нет такого, что для одного исходного текста получаются разные объектные файлы. Один набор текста транслируется всегда в один и тот же машинный код (естественно при неизменных опциях) и правила трансляции всегда встроены в любой компилятор например в backend в gcc.

Посему - утверждаемая ценность компилятора CompCert сомнительна.

А какие критерии корректности компилятора?

Эквивалентность семантики исходного кода и семантики полученного машинного кода.

Компилятор всегда корректен.

Нет, идиот, большинство оптимизаций потенциально некорректны.

Нет такого, что для одного исходного текста получаются разные объектные файлы.

А это-то тут при чем, быдло ты безмозглое?!? Ты хотя бы слово-то такое знаешь, как «семантика»?!?

Посему - утверждаемая ценность компилятора CompCert сомнительна.

Ты грязный и тупой выродок.

Нет, идиот, большинство оптимизаций потенциально некорректны.

Да что вы говорите, вот новость. Не любите оптимизации - не используйте.

А это-то тут при чем, быдло ты безмозглое?!? Ты хотя бы слово-то такое знаешь, как «семантика»?!?

Знаю. И сомневаюсь, что вы понимаете о чём пишите. В любом компиляторе реализован алгоритм взаимно-однозначного соответствия конструкций входного языка выходному при помощи машины состояний. Отсюда и мой вывод про ценность CompCert. Если нет оптимизаций - там вообще всё тривиально для проверки соответствия семантик.

В любом компиляторе реализован алгоритм взаимно-однозначного соответствия конструкций входного языка выходному при помощи машины состояний.

ДОКАЖИ это, грязная швабра.

Если нет оптимизаций - там вообще всё тривиально для проверки соответствия семантик.

Тривиально?!? Докажи хотя бы эквивалентность для элементарных арифметических преобразований, шалава.

gcc, clang, pcc, tcc

ICC

open watcom был

когда целый вызов memset() выкидывается?

и когда он выкидывается? похоже на бред

Тривиально?!? Докажи хотя бы эквивалентность для элементарных арифметических преобразований, шалава.

Если умеете читать код - смотрите в исходный текст компилятора. Если не умеете - не лезьте в чужую область.

В любом компиляторе реализован алгоритм взаимно-однозначного
соответствия конструкций входного языка выходному при помощи
машины состояний.

ДОКАЖИ это, грязная швабра.

RTFM -http://web.eecs.umich.edu/~bchandra/courses/papers/Turbak_6.821/book.pdf

Где там ДОКАЗАТЕЛЬСТВО, ничтожный тупица?

Если умеете читать код - смотрите в исходный текст компилятора. Если не умеете - не лезьте в чужую область.

Все ясно, грязная скотина даже не понимает, что такое ДОКАЗАТЕЛЬСТВО.

ДОКАЖИ, грязная шваль, что «исходный код компилятора» не меняет семантики при преобразованиях. Не забудь при этом, грязная шваль, предварительно формально описать операционную семантику целевого машинного кода.

ДОКАЖИ, грязная шваль, что «исходный код компилятора» не
меняет семантики при преобразованиях. Не забудь при этом,
грязная шваль, предварительно формально описать операционную
семантику целевого машинного кода.

Ну не в теме, а пишешь. Это уже сделано давным-давно и описано в популярной литературе. Поищите в сети документы насчёт machine-description language для gcc и не смеши присутствующих.

Где там ДОКАЗАТЕЛЬСТВО, ничтожный тупица?

Например в материале http://www.eecs.tufts.edu/~dias/dissertation/dissertation.pdf дано много всего на интересующую тему и т.д. и т.п. Учите мат. часть.

Обращение к модераторам - выражения «грязная швабра» «грязная шваль» «грязная скотина» - это нормальная форма общения тут?

Недоумок ты ничтожный. НЕ ДОКАЗАНО сохранение семантики при преобразованиях в GCC.

Прежде чем разевать свою грязную пасть и вонять свои некомпетентные гомосяцкие возражения, тварь, изволь привести свое понимание того, что такое «доказательство». Так, чтоб публика над тобой поржала.

Повторяю для тупой грязи - там НЕТ ДОКАЗАТЕЛЬСТВА. И в коде gcc нет доказтельства. А в коде CompCert доказательства есть. Чуешь разницу, шваль?

Вопрос на засыпку: догадаться, почему CompCert не использует SSA (тогда как gcc и llvm через него проходят). Задача номер два - попытаться придумать, как без зубодробительной сложности доказать тождественность простейших преобразований над SSA. Обломаться. Молиться. Поститься. Слушать радио «Радонежь». Плакать над своей бесцельно прожитой жизнью.

Повторяю для тупой грязи - там НЕТ ДОКАЗАТЕЛЬСТВА. И в коде gcc нет доказтельства.
А в коде CompCert доказательства есть. Чуешь разницу, шваль?

Не чуюю вообще. Привожу дословно из раздела 10.3 для такого, как ты. Конкретно, там автор разъясняет, какие критерии используются для того, чтобы компилятор был корректен - приведено три критерия. Компилятор gcc падпадает под модель SLED. И далее автор для своего компилятора говорит, что будет использовать модель «proof-carrying» в противовес «compiler certification».

In future work, I hope to extend this dissertation to prove that the back ends I generate produce correct code. Because a machine description can be analyzed, it should be possible to write a tool that checks the correct- ness of the machine description. Previous work has already shown how to check the correctness of SLED descriptions (Ferna ́ndez and Ramsey 1997); in future work, I want to devise an algorithm for checking whether a λ-RTL description is an accurate description of the target machine. Furthermore, I would like to prove that each tile in a generated back end produces code that preserves the semantics of the intermediate repre- sentation. There are three main approaches to building provably correct compilers: • Translation validation: Run the tiler and check whether it produces code that maintains the input program’s semantics (Pnueli, Siegel, and Singerman 1998; Necula 2000). • Proof-carrying code: Along with each tile in the generated tiler, in- clude a proof that the tile’s implementation preserves the semantics of the intermediate code (Necula 1997; Morrisett et al. 1999). • Compiler certification: Prove that the code that generates the tile set can only generate semantics-preserving tiles (Leroy 2006). For my purposes, I believe that proof-carrying code is the most practical next step because unlike compiler certification, it does not require rewriting the λ-RTL toolkit in a proof checker, and unlike translation validation, the generated tile set can be checked for correctness independent of any single test program. I hope that I will soon be able to generate back ends for an optimizing compiler that are not just efficient but also provably correct.

Повторяю для тупой грязи - там НЕТ ДОКАЗАТЕЛЬСТВА. И в коде gcc нет доказтельства. А в коде CompCert доказательства есть. Чуешь разницу, шваль?

Ты допускаешь ошибку в логике. Из того, что в CompCert есть доказательство, не следует, что gcc плох или на его модели невозможно доказательство построить или что gcc ошибочен(это твоё утверждение так же не доказывает). Возможны и иные критерии проверки корректности работы компилятора. По-прежнему, учи мат. часть.

Вопрос на засыпку: догадаться, почему CompCert не использует
SSA (тогда как gcc и llvm через него проходят). Задача номер
два - попытаться придумать, как без зубодробительной сложности >доказать тождественность простейших преобразований над SSA. >Обломаться. Молиться. Поститься. Слушать радио «Радонежь». >Плакать над своей бесцельно прожитой жизнью.

Это утверждение значения не имеет, так как мы не говорим об оптимизациях.

Идиот. Во первых, CompCert делает довольно много оптимизаций.

Во вторых, gcc -O0 и llvm без каких либо оптимизаций все равно проходят через SSA.

В третьих, независимо от оптимизаций, там еще и кодогенерация через selection DAG, и у тебя жопа лопнет от натуги, если ты попробуешь доказать его корректность.

Ну и вообще, начнем с того, что у тебя нет вообще формальной семантики машинного кода. И у gcc ее нет. И у llvm ее нет. И ты так до сих пор и не понимаешь даже смысла слова «семантика». Начни с простого: https://en.wikipedia.org/wiki/Operational_semantics

И посмотри на формальную семантику языка Си: https://code.google.com/p/c-semantics/

И подумай еще раз, осилишь ли ты доказать эквивалентность относительно этой семантики всех преобразований в gcc.

Из того, что в CompCert есть доказательство, не следует, что gcc плох

Ты грязный недоумок. Из этого следует, что CompCert гарантированно корректен. И что для gcc никто тебе такой гарантии не даст никогда. Только и всего.

или на его модели невозможно доказательство построить

Практически невозможно. Хотя бы учитывая язык, на котором gcc написан.

или что gcc ошибочен(это твоё утверждение так же не доказывает).

Ты редкостно невменяемое быдло.

Возможны и иные критерии проверки корректности работы компилятора.

Назов их, ничтожество. Ничего более сильного, чем формальное доказательство корректности, быть не может.

По-прежнему, учи мат. часть.

Ну давай, насмеши, расскажи мне про мат. часть. Только не надо больше ссылок на буквари для детского сада, расскажи что-либо интересное. Например, про «иные критерии проверки корректности», отличные от доказательства эквивалентности семантики при преобразовании.

И далее автор для своего компилятора говорит, что будет использовать модель «proof-carrying» в противовес «compiler certification».

Вот когда «будет», тогда и поговорим. Только вот он дальше back end не идет (и, стало быть, практического интереса не представляет), а CompCert тащит корректность от самого исходного AST (только корректность парсера не доказывается).

О том, почему proof-carrying хуже сертификации написано в работах Лероя, просвещайся.

Идиот. Во первых, CompCert делает довольно много оптимизаций.

Тогда ты сам себе противоречишь, когда выше писал про то, что оптимизации - это потенциально некорректная вещь

Во вторых, gcc -O0 и llvm без каких либо оптимизаций все равно проходят через SSA.

Ну и что с того? Отсюда ничего не следует.

И подумай еще раз, осилишь ли ты доказать эквивалентность относительно этой семантики всех преобразований в gcc.

А и не нужно ничего доказывать - можно иные методы проверки корректности использовать, более простые.

Ты грязный недоумок. Из этого следует, что CompCert гарантированно корректен. И что для gcc никто тебе такой гарантии не даст никогда. Только и всего.

Да ничего подобного не следует Из первого утверждение - второе не вытекает вообще. Обычная логика, только и всего. Это вообще не связные вещи.

Практически невозможно. Хотя бы учитывая язык, на котором gcc написан.

Это ошибаешься.

Назов их, ничтожество. Ничего более сильного, чем формальное доказательство корректности, быть не может.

Почитай английский текст, (глава 10.3) - там их приведено 2 кроме «certification»

Нет более простых методов. Ни одного. И уж тем более нет таких методов для всяких там монстров вроде gcc и llvm.

Нет более простых методов. Ни одного. И уж тем более нет таких методов для всяких там монстров вроде gcc и llvm.

Есть. И независимые методы от типа компилятора есть. Например можно построить два графа для переходов - один на основе исходного текста, другой на основе бинарного модуля. В случае отсутствия оптимизаций даже задачу «ИЗОМОРФИЗМ ГРАФОВ» решать не придётся.