LINUX.ORG.RU

Опубликован способ обхода borrow checker в Rust

 


3

10

Jakub Kądziołka опубликовал proof-of-concept, показывающий непосредственные проблемы, связанные с ошибкой в проекте компилятора Rust, которую разработчики безуспешно пытаются решить уже на протяжение четырех лет.

Пример, разработанный Jakub, позволяет обойти Borrow Checker посредством очень простого трюка:

fn main() {
    let boom = fake_static::make_static(&vec![0; 1<<20]);
    println!("{:?}", boom);
}

Разработчик просит не использовать этот обход в Production, так как его целью было только привлечь внимание к проблеме, игнорируемой разработчиками Rust.

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

anonymous

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

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

Что получается, когда разрабатывают языки без разработки соответствующих формальных систем.

Лучший камент. Но судя по опыту php и js, разрабатывавшихся походу вообще без единой мысли в голове, может и взлететь.

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

Что там у поней в этом плане?

Вроде как создатель языка говорил, что у них есть пруфы корректности (смотреть таблицу 5, там про Rust есть интересное)…

shkolnick-kun ★★★★ ()
Последнее исправление: shkolnick-kun (всего исправлений: 3)
Ответ на: комментарий от dimgel

JS разрабатывали впопыхах и кратчайшие сроки, ПХП да, это Перл-курильщика

novikovag ()
Ответ на: комментарий от shkolnick-kun

как можно не проверить i > 0??? как это нажимая Backspace я продолжаю затирать символы в буфере??? Кривизна рук такая???

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

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

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

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

dimgel ★★ ()
Ответ на: комментарий от shkolnick-kun

Причём все 3 конторы одинаково прекрасны.

anonymous ()
Ответ на: комментарий от quantum-troll
forall 'a, 'b, T; &'a &'b (), &'b T -> &'a T where 'b <: 'a
'a = 'static
-----
Ошибка, 'b <: 'static выполняется лишь в случае, когда 'b = 'static

Откуда это? Как это проверить?

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

Когда представится возможность заблудиться в лесу, буду орать: АОООООООООООООЛЛЛЛЛ

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

Откуда это? Как это проверить?

Некое подобие правила вывода, проверять руками (см. TaPL). 'static это подтип для всех лайфтаймов, поскольку &'static T живёт всё время работы программы, и потому его можно передавать в функцию, берущую &'a T.
Вот тут можно почитать про сабтайпинг лайфтаймов: https://doc.rust-lang.org/nomicon/subtyping.html

quantum-troll ★★★★★ ()
Ответ на: комментарий от shkolnick-kun

Я правильно понимаю, что в Rust полно «багов» которые приводят к UB

Да, ты правильно понимаешь - это баги.

это сделано без unsafe, соответственно есть ненулевая вероятность появления «дыр» в «безопасном» коде…

А еще баги в безопасном коде могут появляться из-за багов в компиляторе (и не только в нем). КСЖ.

tailgunner ★★★★★ ()
Последнее исправление: tailgunner (всего исправлений: 1)
Ответ на: комментарий от quantum-troll

Некое подобие правила вывода, проверять руками.

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

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

Интерфейс к тайпчекеру это уже уровень Idris.

Тайпчекер вполне может выводить в smtlib2 формате, который можно скормить smt-solver'у (z3, cvc3/4), и проверить разными движками на правильность. А так, или верить на слово или самому разбираться во внутренностях rust.

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

Баз этих суперкодеров баги бы не выявлялись, кто-то же должен ломать всё. Тем более тут язык как бы в тему. Больше багов найдут, больше исправят, разве это плохо? Раст какашка, но пусть уж лучше будет железобетонная чем иная

LINUX-ORG-RU ()
Ответ на: комментарий от DELIRIUM

Секрет выявления багов в LLVM открыт, ты спалился, так вот почему у тебя животные дома, они были твоими QA !

LINUX-ORG-RU ()
Ответ на: комментарий от RazrFalcon

Напиши тоже самое без синтетики.

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

Т.е. чуваки запилили всё это без какого-либо доказательства корректности?

Я помню, что адепты этой херни носились с доказательствами, а оказывается врали.

К тому же, доказательство не является доказательством. Корректная модель никак не помешает кривой её реализации.

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

Это не линейные типы.

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

Причём тут LLVM?

Непричём это я лично DELIRIUM он был (или есть) разрабом LLVM ))

LINUX-ORG-RU ()
Ответ на: комментарий от RazrFalcon

Реальный код

Ты опять всех напугал!

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

Тайпчекер вполне может выводить в smtlib2 формате, который можно скормить smt-solver'у (z3, cvc3/4), и проверить разными движками на правильность.

Кстати, а есть компиляторы которые такое делают? Я навскидку только внешние приблуды типа frama-c и жидкого хацкелла помню.

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

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

Есть ATS https://github.com/githwxi/ATS-Postiats/ , можно собрать c поддержкой smt2. Компилируется в С-код, без GC. Может в другие языки: js, php, python,...

Есть F* (fstar) https://www.fstar-lang.org/ , который использует z3. Есть подмножество языка Low* (lowstar), который компилирует в С-код (без GC)

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

Язык от человека, который не умеет использовать VCS? Подозрительно.

Он и мейкфайлы писать не умеет. Генерит из текстовых файлов, и не только мейкфайлы, своеобразное недо-«literate programming».

И что?

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

По теме, там десятки таких багов и их никто не скрывает

даже язык не постеснялись назвать соотвествующе

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

Чёт он не собирается

static UNIT: &'static &'static () = &&();

fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v }

fn bad<'a, T>(x: &'a T) -> &'static T {
    let f: fn(_, &'a T) -> &'static T = foo;
    f(UNIT, x)
}

Fixed

q0tw4 ★★★ ()
Ответ на: комментарий от quantum-troll

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

Для дешёвых эффектов было достаточно <blink> и <marquee>, а JS был нужен для alert(), setTimeout() и setInterval(). Чтобы веб-страница тоже могла задрочить посетителя, а не только GUI. Теперь они все не нужны – есть Раст.

kostyarin_ ()

Надо просто запретить неявные условия на типах (foo gets to assume that 'b: 'a). Пусть явно пишут. Тогда хрен забудешь чекнуть при использовании.

fn foo<'a, 'b: 'a, T>(_: &'a &'b (), v: &'b T) -> &'a T { v }

так уже не обойдешь чекер.

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

Вот про F* я что-то слышал, но не пробовал. Надо бы посмотреть. Спасибо, анон.

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

Китайское поделие, что с них взять. Марсиане.

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

Типичный баг с переполнением стэка

ААА, NSA залезает в окно и взламывает грубы, ховайся линуксоиды!

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

Да ну! Даже шаблонная часть плюсов выглядит читабельнее :)

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

Шаблонная часть это какая? Приведи пример плохо-читаемой шаблонной части или объясни в чём заключается «плохо».

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

🌴🌴🌴 🤦🏽‍ 🌴🌴🌴

Глянь внимательнее на фото героя, там есть ответ на твой вопрос…

Я понимаю, никнейм надо оправдывать. Но это уже перебор — как по тупости, так и по жЫрноте. Ещё немного, и СПГС перевалит за уровень «Чудинов/Задорнов».

На фото маечка с TopCoder '2006 — престижного студенческого турнира по программированию. Спонсорами которого, очевидно, были те самые конторы, логотипы которых представлены на рукаве.

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

Это называется удаление гланд через анальное отверстие.

WatchCat ★★★★★ ()

Жесть... Надо ребятам сказать чтоб скорей Perl6 пилили

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

Причём тут перловка? Кагбе языки в разной нише.

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

это что-то типа наколенного std::mem::transmute, но без обязательного для того unsafe?

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

Причём тут перловка?

При том, что

static UNIT: &'static &'static () = &&();

fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v }

fn bad<'a, T>(x: &'a T) -> &'static T {
    let f: fn(&'static &'a (), &'a T) -> &'static T = foo;
    f(UNIT, x)
}

Кагбе языки в разной нише.

Это ниша write-only code аля сделал&забыл.

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

Это ниша write-only code аля сделал&забыл.

Нет такой ниши, ты её выдумал.
Перл это скриптовый язык, а Раст это компилируемый язык.
И они не пересекаются кроме как через FFI.

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

пример плохо-читаемой шаблонной части

Классика же:

        template                                                                
        <                                                                       
            typename T1  = NullType, typename T2  = NullType, typename T3  = NullType,
            typename T4  = NullType, typename T5  = NullType, typename T6  = NullType,
            typename T7  = NullType, typename T8  = NullType, typename T9  = NullType,
            typename T10 = NullType, typename T11 = NullType, typename T12 = NullType,
            typename T13 = NullType, typename T14 = NullType, typename T15 = NullType,
            typename T16 = NullType, typename T17 = NullType, typename T18 = NullType
        >                                                                       
        struct MakeTypelist                                                     
        {                                                                       
        private:                                                                
            typedef typename MakeTypelist                                       
            <                                                                   
                T2 , T3 , T4 ,                                                  
                T5 , T6 , T7 ,                                                  
                T8 , T9 , T10,                                                  
                T11, T12, T13,                                                  
                T14, T15, T16,                                                  
                T17, T18                                                        
            >                                                                   
            ::Result TailResult;                                                
                                                                                
        public:                                                                 
            typedef Typelist<T1, TailResult> Result;                            
        };

Хотя в целом всё понятно =)

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

Потому что на ЛОРе убогая клиентская синтаксическая подсветка на основе highlight.js

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

Так и на Расте всё понятно.
Просто большинство укушено Сишечкой и ломаются на одиночной кавычке. Меня тоже долго ломало, но это дело привычки.
Вообще конечно IMHO не лучший вариант для обозначения времени жизни, но теперь уже поздняк метаться.

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

NullType

Что это за говно? Никакой адекватный крестовик подобное именование идентификаторов не использует.

Result

Это вообще биомусор, ведь человек никогда не будет писать локалы с большой буквы.

typename T1

Это херня дошколятская. С года 8-9 есть вариадики.

Ну в целом это примитивная херня. Ничего от С++ тут нет. Базовый синтаксис определения параметров, дефолтная инициализация через равно. Дефолтный тайпдеф, в целом тут разница между сишным/не сишным тайпдефом минимальна.

>                                                                   
            ::Result 

В таком стиле адекватные люди так же не пишут.

Это не С++ и это писал не человек.

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