URL: https://www.opennet.me/cgi-bin/openforum/vsluhboard.cgi
Форум: vsluhforumID3
Нить номер: 88526
[ Назад ]

Исходное сообщение
"В рамках проекта SMACK развивается новая система статической..."

Отправлено opennews , 04-Фев-13 21:42 
В списке рассылки разработчиков LLVM представлен (http://lists.cs.uiuc.edu/pipermail/llvmdev/2013-February/058...) новый проект SMACK (http://smackers.github.com/smack/), в рамках которого создан инструмент для статической проверки свойств программ, написанных на языках  C/C++. На основании анализа исходных текстов программы, без непосредственного выполнения приложения, SMACK позволяет выявить нарушение заданных пользователем  утверждений корректности (assertions (https://github.com/smackers/smack/tree/master/examples)).


Код инструмента поставляется (https://github.com/smackers/smack) под лицензией MIT и интегрируется с инфраструктурой компиляции LLVM. При желании SMACK может быть выведен за рамки C/C++ и после небольшой доработки использован для проверки кода на любом другом языке программирования, поддерживаемом в LLVM. Также возможно создание расширений, работающих поверх SMACK.

URL: http://lists.cs.uiuc.edu/pipermail/llvmdev/2013-February/058...
Новость: http://www.opennet.me/opennews/art.shtml?num=36023


Содержание

Сообщения в этом обсуждении
"В рамках проекта SMACK развивается новая система статической..."
Отправлено x0r , 04-Фев-13 21:42 
побыстрей бы clang checker допилили до C++...

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Аноним , 04-Фев-13 23:12 
Что только не сделают, лишь бы хаскелл не учить.:)

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Аноним , 04-Фев-13 23:28 
Так где ваши ядра операционок на хаскелле, сэр?

"В рамках проекта SMACK развивается новая система статической..."
Отправлено BratSinot , 05-Фев-13 01:20 
http://web.archive.org/web/20041117045537/http://www.macs.hw.../

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Аноним , 05-Фев-13 03:04 
> http://web.archive.org/web/20041117045537/http://www.macs.hw.../

Оно настолько живет и процветает что даже пришлось использовать веб-архив? А что, вы не хотите пользоваться этим? Надо же, какая незадача. Круто придумано - пытаться впаривать ДРУГИМ то что не хочешь жрать САМ.



"В рамках проекта SMACK развивается новая система статической..."
Отправлено scor , 05-Фев-13 09:35 
>> http://web.archive.org/web/20041117045537/http://www.macs.hw.../
> Оно настолько живет и процветает что даже пришлось использовать веб-архив? А что,
> вы не хотите пользоваться этим? Надо же, какая незадача. Круто придумано
> - пытаться впаривать ДРУГИМ то что не хочешь жрать САМ.

Не нравится hOp из веб-архива? Ну вот вам House http://programatica.cs.pdx.edu/House/. Вполне себе из "интернета".:)
А вообще, в чём претензия? Вы задали вопрос: "есть ли ядра на хаскеле?" Вам доказательно ответили, что есть. Или вы имели ввиду: "есть ли <ядро моей любимой ОС> на хаскеле?":)


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 05-Фев-13 19:18 
Обычно в таких случаях подразумевается "есть ли актуальное, развивающееся, где-то реально применяемое"...

"В рамках проекта SMACK развивается новая система статической..."
Отправлено scor , 05-Фев-13 23:09 
> Обычно в таких случаях подразумевается "есть ли актуальное, развивающееся, где-то реально
> применяемое"...

Тогда нужно определиться в терминологии и контексте. Если имелись ввиду _именно_ ядра, то утвердительный ответ был дан. Если же имелось ввиду "низкоуровневое" программирование, как таковое, то и тут есть эволюция hOp -> House -> HaLVM (https://github.com/GaloisInc/HaLVM). Правда не знаю, послужили ли два предыдущих проекта основой для последнего, но толчком уж точно явились. Так что даже в этой области у функциональщиков не всё так плохо.:)

PS. Собственно были даже попытки писать модули для Linux на хаскеле (http://www.haskell.org/haskellwiki/Kernel_Modules). Но это скорее proof-of-concept, т.е. можно, но зачем, если есть C?


"В рамках проекта SMACK развивается новая система статической..."
Отправлено AnonymousSL , 05-Фев-13 16:14 
А где ядра операционок на C++, мэм?

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 05-Фев-13 18:55 
навскидку вспоминается ядро NT. Но если не нравится - полуось. Мргучая вещь была, кстати.

"В рамках проекта SMACK развивается новая система статической..."
Отправлено scor , 05-Фев-13 23:01 
> навскидку вспоминается ядро NT. Но если не нравится - полуось. Мргучая вещь
> была, кстати.

Немного противоречит вашему же #28.:) Они может где-то и применяются, но вот развивающимися и актуальными я бы их не назвал.:)


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 06-Фев-13 04:30 
NT вполне себе актуально. Просто здесь его некоторые активно не любят по понятным причинам, но ядро, насколько я знаю, неплохое.

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Vkni , 06-Фев-13 15:48 
> NT вполне себе актуально. Просто здесь его некоторые активно не любят по
> понятным причинам, но ядро, насколько я знаю, неплохое.

Очень хорошее ядро. Позволяет, в частности, построить поверх себя POSIX, OS/2, Win32 и т.д.


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Aesthetus Animus , 06-Фев-13 00:13 
> А где ядра операционок на C++

L4


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 05-Фев-13 02:39 
Угу, язык равно чужеродный как для человека, который должен на нём писать, так и для машины, которая должна его исполнять. Зато красивые математические абстракции, угу.

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 05-Фев-13 02:53 
Да, реплика у меня холиворная получилась, но это случайность - я не против хаскеля или функциональщины. Я всего лишь против её применения в продакшне в чистом виде. А вот как отдельные элементы она живёт отлчино - вон, всякие map уже давно норма. Внутри императивщины.

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Аноним , 05-Фев-13 03:06 
> Да, реплика у меня холиворная получилась,

...но суть дела отражает неплохо. Поэтому чего стесняться то?


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Аноним , 05-Фев-13 07:38 
> Я всего лишь...

...ламо. Мы уже поняли.


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Vkni , 05-Фев-13 09:25 
> Угу, язык равно чужеродный как для человека, который должен на нём писать,
> так и для машины, которая должна его исполнять. Зато красивые математические
> абстракции, угу.

C++ не менее чужероден.


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Аноним , 05-Фев-13 16:06 
>C++ не менее чужероден.

По каким критериям, мальчик?


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 05-Фев-13 18:58 
Вы б хоть погуглили прежде чем хамить...

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 05-Фев-13 18:53 
Плюсы странны, но ровно по двум причинам. Во-первых, совместимость с С. Благодаря ей плюсы вообще взлетели, но красоты им она не добавляет. Во-вторых, ориентация на системщину, из-за которой, скажем, GC жестко прибивать нежелательно, а без него некоторые удобства не сделать.

Но в принципе императивный подход - он же естественен до безобразия, люди от века составляли разные инструкции, в которых и ветвления были, и циклы... Например, представьте, как будете объяснять кому-то как взвесить килограмм сахара - всё будет.


"В рамках проекта SMACK развивается новая система статической..."
Отправлено тоже Аноним , 05-Фев-13 20:02 
> императивный подход - он же естественен до безобразия

Причем как для человека, так и для компьютера. Все более высокоуровневые завихрения все равно выстраиваются в очередь перед процессором. Плюсы, в отличие от языков со всеми удобствами, позволяют этой очередью хоть как-то управлять.


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Vkni , 06-Фев-13 04:02 
> Плюсы, в отличие от  языков со всеми удобствами, позволяют этой очередью хоть как-то управлять.

Чаще всего это низкоуровневое управление не только нежелательно, а прямо таки вредно.


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 06-Фев-13 04:23 
Дык там, где вредно - не берите плюсы, какие проблемы? Вон, в том же D или питоне или C# на худой конец всё это низкоуровневое скрыто.

"В рамках проекта SMACK развивается новая система статической..."
Отправлено scor , 05-Фев-13 22:57 
> ...люди от века составляли разные инструкции, в которых и ветвления были, и циклы...

Только, как правило, все эти алгоритмы преследуют своей целью не выполнить некоторые действия ради выполнения этих действий, а получить некий результат от их выполнения. В этом и есть фундаментальная разница подходов и мышления: можно описывать алгоритм получения результата, а можно описывать сам результат. Всё сводится к поставленной задаче.

> Например, представьте, как будете объяснять кому-то как взвесить килограмм сахара - всё будет.

Вопрос подходов.:) Например, можно так: на одной чаше весов лежит эталонный киллограмм, а на другой сахар. Показания стрелки весов и есть ответ на вопрос: "сахар весит больше, меньше или ровно киллограм".

data Indicator = Center
               | ReferenceSide
               | SugarSide

type Result = String

is1Kg :: Indicator -> Result
is1Kg Center          = "exact 1Kg!"
is1Kg ReferenceSide   = "less than. add more sugar"
is1Kg SugarSide      = "too mutch. remove some sugar"

*Main> is1Kg ReferenceSide
"less than. add more sugar"
*Main> is1Kg SugarSide
"too mutch. remove some sugar"
*Main> is1Kg Center
"exact 1Kg!"
*Main>

Ваш императивный вариант будет проще в понимании?:)


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 06-Фев-13 04:02 
Конечно проще. Здесь же натуральное изменение переменной, никакой иммутабельности.


empty(scales.right_cup);
scales.left_cup - WEIGHT_1_KG;
add_some(SUGAR, scales.right_cup);
do {
   ;
   if (scales.arrow.is_at_left())
     add_some(SUGAR, scales.right_cup);
   else if (scales.arrow.is_at_right)
     remove_some(SUGAR, scales.right_cup);
   else
    exit(0);
} while(1);

описывает ровно то, что делает человек. Читабельно даже если вообще ЯП не знать (для таких специально exit а не break поставил).


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Vkni , 06-Фев-13 04:01 
> Плюсы странны, но ровно по двум причинам.

Не только этим. Слишком сложный подход к шаблонам, к примеру. Груда костылей, связанных с историей.

> Но в принципе императивный подход - он же естественен до безобразия, люди
> от века составляли разные инструкции, в которых и ветвления были, и
> циклы...

Так императивный подход - это в С. С++ - объектно-ориентированный (это неестественная вещь) и "обобщённый" (сделан несколько костыльно и неудобно).

> Например, представьте, как будете объяснять кому-то как взвесить килограмм сахара
> - всё будет.

Мне формулы писать тоже естественно. Опять-таки, после некоторой практики ловлю себя на том, что писать

let iter factorial x =
    if x > 0 then
         x*(factorial (x - 1))
    else
        1;;

мне "приятнее" чем через цикл.


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 06-Фев-13 04:14 
ООП тоже абсолютно естественно :-) Мы всю свою жизнь проводим, как-то взаимодействуя с чем-то, что мы выделили в среде как объекты, затем либо активно запрашиваем их состояние (глазками смотрим, ушками слушаем и т.п.) либо ждём,когда они нам как-то просигналят.

ООП на примере. Есть у нас автомобиль. В нём - место для магнитофона.

Магнитофон,понятное дело, реализует стандартные интерфейсы (форм-фактор, питание, колонки, интерфейс пользователя - те самые кнопочки - перемотка вперед-назад, старт/стоп, пауза). Он инкапсулирован - мы можем заменить его, скажем, на CD-плеер или mp3-проигрыватель (вот вам полиморфизм) и всё подключится точно также и кнопочки будут такими же, и машину нам для этого модифицировать не надо. Он может реализовывать дополнительный интерфейс - быть радиолой. Тогда его потребитель может этот интерфейс использовать, может - не использовать, но ничего другого это не коснётся.

Наследования здесь нет, и это тоже важно - наследование, вообще говоря, является деталью реализации и отнюдь не обязательно (что в плюсах и дают дженерики, сделанные, согласен, криво).

А вот насчёт приятнее - это уже вопрос другой. Но - "после некоторой практики". И компьютеру (который не иммутабельный нги разу) придётся потом проделывать обратную операцию и разворачивать эту штуку в цикл. Хотя нет - эта не развернется, это ж не хвостовая рекурсия... будет стек создавать зачем-то...


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Vkni , 06-Фев-13 05:23 
> ООП тоже абсолютно естественно :-) Мы всю свою жизнь проводим, как-то взаимодействуя
> с чем-то, что мы выделили в среде как объекты, затем либо
> активно запрашиваем их состояние (глазками смотрим, ушками слушаем и т.п.) либо
> ждём,когда они нам как-то просигналят.

Хорошо, неестественно наследование. Неестественны виртуальные функции. Так что тут мы с вами соглашаемся.


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 06-Фев-13 17:01 
ну да, это трудно понимаемый кусок, помню с каким трудом въезжал - ещё на паскале... Но он довольно невелик и далеко не всегда нужен, если брать не яву какую.

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Vkni , 06-Фев-13 17:50 
> ну да, это трудно понимаемый кусок, помню с каким трудом въезжал -
> ещё на паскале... Но он довольно невелик и далеко не всегда
> нужен, если брать не яву какую.

Алекс, по моему опыту, переход на по-настоящему новые приёмы всегда приводит к мозголомке. У меня она была при изучении процедурного програзма, потом ОО, потом шаблонов, потом функциональщины. Я просто помню эти мозголомки, поэтому мне кажется это всё неестественным.

А дальше, как привыкнешь, уже всё кажется в доску естественным и правильным.


"В рамках проекта SMACK развивается новая система статической..."
Отправлено scor , 06-Фев-13 09:57 
> Хотя нет - эта не развернется, это ж не хвостовая рекурсия... будет стек создавать зачем-то...

Тут вы правы. Гораздо читабельней и эффективней будет так:
let fac n = product [1..n]

Понять, что тут произойдёт и чему равен результат сможет почти кто угодно.:)


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 06-Фев-13 04:35 
Да, насчет шаблонов. Они в плюсах редкая гадость (кстати,  в основном из-за того, что их попытались сделать функциональными - в D вон императивщина - удобная и понятная). Но сложная писанина на них, в общем-то, простым смертным особо и не требуется, это для разных авторов бустов и подобного.

А простой template class MyClass<class T> :public T {...} наваять - ничего сложного, в общем-то. Простейшую шаблонную функцию - аналогично. Вон каноничный простейший пример:
template <typename Type> Type max(Type a, Type b) {
    return a > b ? a : b;
}

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


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Vkni , 06-Фев-13 05:27 
> А простой template class MyClass<class T> :public T {...} наваять - ничего
> сложного, в общем-то.

Алекс, наваять и метапрограммную фигню на них несложно. Сложно это читать. :-)

Там, в шаблонах масса всяких косяков. Например, в С++98 целое число может быть параметром шаблона, а вещественное - нет.


"В рамках проекта SMACK развивается новая система статической..."
Отправлено scor , 06-Фев-13 09:31 
сложного ничего конечно, но работает не так, как, очевидно, ожидается.:)
чему равна в этом случае:
max(1, 2.3);
очевидно, что должно быть:
max(1, 2.3) == 2.3
но компилятор не согласен:)
error: no matching function for call to 'max(int, double)'
note: candidate is:
note: template<class Type> Type max(Type, Type)
note: template argument deduction/substitution failed
note: deduced conflicting types for parameter 'Type' ('int' and 'double')

в отличии от:
Prelude> :t max
max :: Ord a => a -> a -> a
Prelude> max 1 2
2
Prelude> max 1.0 2
2.0
Prelude> max 1 2.0
2.0
Prelude> max 1 (2/3)
1.0
Prelude> :t 1
1 :: Num a => a
Prelude> :t 2.0
2.0 :: Fractional a => a
Prelude> :t (2/3)
(2/3) :: Fractional a => a
можно и явно указать, что мы хотим получить в результате:
Prelude> max 1 (2.0 :: Double)
2.0
Prelude> :t max 1 (2.0 :: Double)
max 1 (2.0 :: Double) :: Double

Ну это я уже придираюсь видимо.:)


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 06-Фев-13 17:04 
ох, наверное, да. В вашем примере же правила приведения какие-то отрабатывают, я так понимаю? Тут я даже не уверен, какой вариант предпочту - всё же автоматическое примедение типов иногда делает те ещё подляны. Кстати, а что будет, если одним из аргументов вам сунуть не Double, а функцию или строку?

"В рамках проекта SMACK развивается новая система статической..."
Отправлено scor , 06-Фев-13 18:01 
> В вашем примере же правила приведения какие-то отрабатывают, я так понимаю?

http://www.ibm.com/developerworks/ru/library/l-haskell2/inde...-
Типы не приводятся автоматически, они могут выводятся, исходя их контекста написанного выражения.
Prelude> :t max
max :: Ord a => a -> a -> a
В данном случае тип выражения наиболее общий. Любой тип, который может быть упорядочен (Ord), т.е. для которого определена функция "compare". Но тип двух аргументов и результата должен быть одинаков.
Prelude> :t max 1
max 1 :: (Num a, Ord a) => a -> a
Тут мы уже более конкретизировали наши намерения. Помимо Ord, мы ещё хотим, чтобы аргумент относился к классу чисел (Num), для которого определены функции: +, -, * и взятие абсолютного значения (abs).
Prelude> :t max 1.2
max 1.2 :: (Fractional a, Ord a) => a -> a
Более конкретно. Мы хотим тип для которго определено значение функции / "разделить".
Prelude> :t max 'a'
max 'a' :: Char -> Char
Тут мы хотим тип Char, для которого определена операция сравнения и соответственно мы можем определить какой из аргументов больше.

Примерно также могли бы поступать и шаблоны в c++. Но видимо были на то какие-то веские основания так не делать.

> Кстати, а что будет, если одним из аргументов вам сунуть не Double, а функцию или строку?

Тип выражения не получиться вывести автоматически, т.к. 1 нельзя выразить типом Char, а 'A' нельзя выразить типом из класса Num.
Prelude> max 1 'A'
No instance for (Num Char) arising from the literal `1'
Possible fix: add an instance declaration for (Num Char)

ЗЫ. Мог запутаться в терминологии. Не хаскелл-гуру я пока.:)


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Vkni , 06-Фев-13 21:08 
> Примерно также могли бы поступать и шаблоны в c++. Но видимо были
> на то какие-то веские основания так не делать.

Хаскелл появился через год после введения шаблонов в С++.


"В рамках проекта SMACK развивается новая система статической..."
Отправлено scor , 05-Фев-13 09:29 
> Угу, язык равно чужеродный как для человека, который должен на нём писать, так и для машины, которая должна его исполнять. Зато красивые математические абстракции, угу.

http://code.google.com/p/hedgewars/source/browse/#hg/gameServer
Вроде и люди пишут, но и машины понимают. И это даже работает.:)

ЗЫ. А абстракции действительно годные.:)


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Crazy Alex , 05-Фев-13 18:54 
Дык, всегда найдётся кто-то со странно завернутыми мозгами :-) А уж о безумии математиков легенды ходят.

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Аноним , 05-Фев-13 00:30 
AddressSanitizer: a fast memory error detector

http://code.google.com/p/address-sanitizer/


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Путин В.В. , 05-Фев-13 03:48 
Адресной дизинфектор уже давно включен в состав clang. Просто компиляете проект с нужными опциями. Но адресной_сатана нужен только тогда когда ваша программа падает. Это не утилита для проверки кода.

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Аноним , 05-Фев-13 04:31 
Спасибо за описание, но какие флаги нужны для его вкомпиляции ?

"В рамках проекта SMACK развивается новая система статической..."
Отправлено arka , 05-Фев-13 07:52 
Там же в вики - http://code.google.com/p/address-sanitizer/wiki/Flags

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Аноним , 05-Фев-13 07:39 
> Адресной дизинфектор уже давно включен в состав clang

И с какой же версии?

> Просто компиляете проект с нужными опциями

И с какими же?


"В рамках проекта SMACK развивается новая система статической..."
Отправлено Клыкастый , 05-Фев-13 09:57 
http://clang.llvm.org/docs/AddressSanitizer.html

"В рамках проекта SMACK развивается новая система статической..."
Отправлено Аноним , 05-Фев-13 09:57 
boost уже проходит валидацию этим SMACK-ом?

"В рамках проекта SMACK развивается новая система статической..."
Отправлено const86 , 05-Фев-13 16:07 
Сначала SMACK должен пройти боевое крещение бустом :)

"В рамках проекта SMACK развивается новая система статической..."
Отправлено anonymous , 05-Фев-13 13:58 
Static analysis of C/C++ code. Checks for: memory leaks, mismatching allocation-deallocation, buffer overrun, and many more.
http://sourceforge.net/projects/cppcheck/

"В рамках проекта SMACK развивается новая система статической..."
Отправлено EuPhobos , 05-Фев-13 20:17 
А Макаревич будет?