- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
Function/method calling convention. Here’s a simple example:
struct Foo { a: i32 }
impl Foo { fn bar(&mut self, val: i32) { self.a = val + 42; } }
fn main() {
let mut foo = Foo { a: 0 };
foo.bar(foo.a);
}
For now this won’t compile because of the borrowing but shouldn’t the compiler be smart enough to create a copy of foo.a before call?
I’m not sure but IIRC current implementation first mutably borrows object for the call and only then tries to borrow the arguments.
Is it really so and if yes, why?
Update: I’m told that newer versions of the compiler handle it just fine but the question still stands (was it just a compiler problem or the call definition has been changed?).
The other thing is the old C caveat of function arguments evaluation. Here’s a simple example:
let mut iter = “abc”.chars();
foo(iter.next().unwrap(), iter.next().unwrap(), iter.next().unwrap());
So would it be foo('a','b','c') or foo('c','b','a') call. In C it’s undefined because it depends on how arguments are passed on the current platform
(consider yourself lucky if you don’t remember __pascal or __stdcall).
In Rust it’s undefined because there’s no formal specification to tell you even that much.
And it would be even worse if you consider that you may use the same source for indexing the caller object like
handler[iter.next().unwrap() as usize].process(iter.next().unwrap()); in some theoretical bytecode handler
(of course it’s a horrible way to write code and you should use named temporary variables but it should illustrate the problem).
Follow us!
То есть в спецификации языка, про которую numухи с гордо раздутыми щеками numушились, что, мол, они ма-те-ма-ти-чес-ки доказали её корректность, попросту отсутствуют настолько важные детали? Блядь, они там ма-те-ма-ти-чес-ки доказывали корректность макроса «println!» что ли?
Ну да, охуенный способ «убрать» UB: неопределённые кейсы просто не будем включать в спецификацию. Смекалочка!
Сам удивился находчивости пuтушатников.
Но статья утверждает никакой формальной спецификации rust вообще не существует!
First and foremost, Rust does not have a formal language specification and by that I mean that while some bits like grammar and objects are explained, there are no formal rules to describe what language features can and cannot be. If you’ve ever looked at ISO C standard you’ve seen that almost any entity there has three or four parts in the description: formal syntax, constraints (i.e. what is not allowed or what can’t be done with it), semantics (i.e. what it does, how it impacts the program, what implementation caveats are there), and there may be some examples to illustrate the points. The best close equivalent in Rust is The Rust Reference and e.g. structure there is described in the following way: syntax (no objections there), definition in a form of “A struct is a nominal struct type defined with the keyword struct.”, examples, a brief mention of empty (or unit-like) structures in the middle of examples, and “The precise memory layout of a struct is not specified.” at the end. I understand that adding new features is more important than documenting them but this is lame.
A proper mature language (with 1.0 in its version) should have a formal specification that should be useful both for people developing compilers and the programmers trying to understand certain intricacies of the language and why it does not work as expected (more on that later).
Конечно смешно говорить о каких-то «спецификациях», если есть одна говнореализация на ворованной инфраструктуре (LLVM).
И никаких альтернативных компиляторов, как это принято в открытых системах. Одна пропаганда.
Какая спецификация, лол. Первые версии раста, емнип, вообще были что-то типа окамла с иммутабельностью и гц, и что из этого вышло.
И в ней отсутствует чёткая спецификация. Точнее спекой раста является постоянно меняющаяся референсная реализация, основанная на крестовой платформе (!) с кучей своих багров.
> Первые версии раста, емнип, вообще были что-то типа окамла с иммутабельностью и гц
Это ещё можно как-то списать на детские болезни, бета-релизы.
Оно и понятно, ведь спецификации пишут только древние сишники, мерзкие крестобляди и прочие скучные джависты. Нормальному языку спецификация как телеге пятое колесо.
Зацени ещё вот это.
Ма-те-ма-ти-чес-ки доказали корректность. Но не в терминах С++.
Then there’s LLVM dependency. I understand that LLVM provides many advantages (like no need to worry about code generation for many platforms and optimising it) but it gives some disadvantages too. First, you don’t have a really self-hosting compiler (a theoretical problem but still a thing worth thinking about; also consider that you have to rely on a framework developed mostly by large corporations mostly in their own interests). Second, you’re limited by what it does e.g.
I read complaints about debug builds being too slow mostly because of LLVM backend. And I suspect it still can’t do certain kinds of memory-related optimisations because it was designed with C++ compiler in mind which still has certain quirks regarding multiple memory access (plus IIRC there was one LLVM bug triggered by an infinite loop in Rust code that’s perfectly valid there but not according to C++ rules). I’m aware that cranelift exists (and Rust front-end for GCC) so hopefully this will be improved.
И тут мы приходим к тому, о чём я уже говорил...
#скрылвореции
This defines an anonymous function containing an infinite loop, and calls it. Any sane compiler would make this just loop forever, right?
Yeah, that's right. In Rust, an ostensibly safe language, Clang's overeager optimizer chooses to emit an illegal instruction in lieu of an infinite loop.
This particular bug actually comes from C++. In C++, threads may be assumed to always make forward progress, i.e. side-effect-free infinite loops are UB.
However, this is not true in C, and it's definitely not true in Rust, yet Clang makes this assumption anyway.
It gets a lot worse; once Clang sees an infinite loop and decides it's UB, it gets to make all sorts of thoroughly invalid and silly "optimizations"; see this SO question for some examples:
https://stackoverflow.com/questions/59925618/how-do-i-make-an-infinite-empty-loop-that-wont-be-optimized-away
Имхо, в спеке безопасного языка эта конструкция вообще должна быть запрещена. И конпелятор должен выдавать ошибку до того, как отправит её в llvm. Потому что в 100% случаев пустой бесконечный цикл - это баг.
Какие глупости )))
Кому это надо? Программист ведь не дурак и знает что делает.
Вот именно поэтому языка от bormanda и нет
А жаль. сорян, у меня зелёной краски в обрез
> конпелятор должен выдавать ошибку до того, как отправит её в llvm
rust-конпелятор отлавливает серьёзные ошибки™, а не такую чепуху.
К слову Swift тоже обосрался.
https://blog.regehr.org/archives/1467
https://bugs.swift.org/browse/SR-3016
Где можно прочитать об этом в спеке?
Нет способа завершить такой цикл не выходя за рамки языка. Тред, который дойдёт до этого цикла, гарантированно никогда не завершится. Именно поэтому шланг подумал, что этот код недостижим и воткнул туда ud2.
И, скорее всего, в расте нельзя просто так взять бросить тред, надо его заджойнить. Безопасный же язык. Т.е. теперь и вся программа в целом гарантированно никогда не завершится. Именно поэтому безопасный язык должен реджектить такую конструкцию.
> знает что делает
Тогда он бы добавил в цикл hlt или wfi. Какое-нибудь sha256() в конце-концов, если ему проц погреть хотелось.
Хотя и это безопасный конпелятор, имхо, имеет право зареджектить (но не обязан, т.к. он не может решить задачу останова).
Да там же весь комент зелёный, о чём сообщает спойлер.
Я в таком восторге от rusta, что зелёной краски просто не хватило.
Понятно же, что программист — дурак и непременно напишет какую-то хуйню.
Там люди занимаются делом, а не тупым самопиаром и сказками про «ма-те-ма-ти-чес-кую ко-ко-ко-ректность».
Но пропаганда никогда не расскажет и не покажет этого лалкам.
Поверх структурной рекурсии сделан сахарок Program ... {measure X}, который позволяет измерять количество оставшихся шагов рекурсии. Если докажешь, что на каждом шаге это число убывает, то молодец (и Coq за структурный аргумент примет это число).
З.Ы. Но смогу написать конпелятор.
Да. Если бы Coq был Тьюринг-полным, в нём можно было бы доказать False, и цена была бы ему грош. (Поэтому я скептически смотрю на зависимые типы в LiquidHaskell и т.п.).
Обходных вариантов много. Можешь описать операционную семантику брейнфака, написать функцию, которая делает один шаг интерпретатора, и экстрагировать её в ocaml. Можешь использовать её для доказательства свойств программ или написания сертифицированного компилятора. Можешь зациклить её с помощью Ltac. Метушня-то как раз там Тьюринг-полная.
Axiom mov_copies_src_to_dst:
forall s : state, src dst : reg,
get dst (mov src dst s) = get src s.
Axiom mov_affects_only_dst:
forall s : state, src dst r : reg, r <> dst ->
get r (mov src dst s) = get r s.
Я бы аксиомами в принципе не баловался, т.к. они позволяют всё сломать. Я не настоящий сварщик, просто книжку нашёл, но сайд-эффекты моделировал бы логикой Хоара (или более продвнутым её вариантом, Separation Logic), и всё описывал бы обычными индуктивными типами. В модел-чекере, который я от скуки пилю, все состояния и все переходы так закодированы: https://github.com/k32/libtx/blob/master/theories/Handlers/MQ.v#L54
Почему, кстати? Питуринговая полнота разве не про вычислимые функции?
В логике Coq False — тип без конструкторов, который играет огромную роль. Термы этого типа не существуют, и поэтому с их помощью можно определить логическое НЕ: "not A := A -> False" (Из A следует несуществующая херь, поэтому A — несуществующая херь). Поэтому любая дыра, позволяющая создать терм с типом False — это мгновенный пиздец любой непротиворечивости.
Походу в крестах его не просто так в UB'ы записали.
Скорее, что доказывать что-либо _на_ расте (а не _о_ нём) — очень плохая идея. Что можно доказать _о_ языке с такими циклами, вопрос сложный, ответ я не знаю.
А нужна ли для питуринговой полноты бесконечная рекурсия? Она же не нужна для вычисления какой-либо вычислимой функции. Так что в теории, как я вижу, можно иметь питуринг-полный язык, в котором невозможен вечный цикл. А вот как его сделать и не напороться на проблему останова — хз.
Рекурсии в Тьюринг-полном языке в принципе может не быть (в нём может не быть функций, к примеру), но должен быть тот или иной способ создать программу, которая никогда не завершится. Все Тьюринг-полные языки должны быть эквивалентны, т.е. на любом ТП языке можно написать интерпретатор другого ТП языка. И если брейнфак умеет виснуть, то и хост язык тоже должен это уметь.
Каким образом так получается, что на Coq можно написать функцию, делающую один шаг интерпретатора, но сам интерпретатор написать нельзя? По-моему это хуйня какая-то. Ну вот допустим я доказываю теорему про программу на брейнфаке, мне надо доказать, что вполне конкретная брейнфак-программа всегда завершится на каком-то шаге. Что я делаю - я просто N раз применяю функцию "сделай-один-шаг", ну типа step( step(.... step(step(step(step(BF_INITIAL_STATE))) ...)) и показываю, что на таком-то вот шаге выполняется условие останова. Интерпретировать пошагово для доказывания некоторой хуйни вполне можно, значит интерпретатор есть, и написать его можно.
Как я понял, потому что на коке нельзя написать функцию, которая никогда не завершится. То есть выполнить «+[[>+]>[+>]+]» — полностью валидную программу на «Brainfuck» — не получится. Из этого же следует, что кок не полон по Питурингу.
> я просто N раз применяю функцию "сделай-один-шаг"
Этим ты докажешь только то, что за N шагов указанная программа либо завершится, либо нет. Провал доказательства не будет обозначать ровным счётом ничего (программа может как никогда не завершиться, так и просто закончиться через N + 1 шагов).
Только если ты можешь доказать, что каждый шаг приближает тебя к остановке. Если не можешь - такой интерпретатор тупо не сконпелируется.
Для произвольной программы на брейнфаке ты этого доказать, само собой, не можешь. Но для какого-то подмножества программ, наверное, можно.
Ну так можно написать стратегию на какой-нибудь вспомогательной питушне для Coq, которая будет до усрачки применять интерпретатор к стейту брейнфак-машины, пытаясь дойти до состояния останова, и такая стратегия в процессе своей работы вполне может зависнуть. И вот она уже будет полной по Тьюрингу, осталось только найти компьютер с бесконечной оперативкой, на которой такая стратегия может реально вечно работать
Coq требует, чтобы все функции были тотальными, т.е. для каждого набора аргументов был результат. Тьюринг-полные языки (включая brainfuck) фундаментально не тотальны, т.к. умеют бесконечно зацикливаться и не возвращать ничего.
Один шаг интерпретатора брейнфака можно представить как тотальную чистую функцию: (память, IP, IO buffers) -> (память, IP, IO buffers). С этим проблем нет. Но чтобы выполнить N шагов интерпретатора, тебе нужно _заранее_ знать N, чтобы передавать его в цикл интерпретатора на Gallina. Потому что в Gallina рекурсия обязана делать паттерн-матчинг на каком-то одном аргументе функции, и рекуррентно вызываться только для полученных из него подтермах (выше я постарался объяснить почему). В общем случае такого N нет.
- цикл должен перед ] возвращать курсор в то же место, где он был при [
- цикл должен монотонно уменьшать или увеличивать свою ячейку на 1
- цикл не должен менять ячейки, которые находятся слева
Здесь я могу по индукции доказать, что каждый шаг самый правый цикл приближается к нулю. А когда он резетится, он приближает к нулю предыдущий цикл. Поскольку код конечен, любая такая прога сможет завершиться.
Я смогу сказать, что мой интерпретатор существует только для такого подмножества? Ну и дальше пусть вызывающий код доказывает, что прога действительно подчиняется этим правилам.
И назвать новый язык Total brainfuck. Можно ещё разрешить бесконечные циклы, которые гарантированно делают I/O, и запилить интерпретатор на корекурсии. С её помощью в gallina можно бесконечно зацикливаться, но только если ты на каждой итерации _приделывашь_ к структурному аргументу новый конструктор, т.е. выполняешь процесс, обратный структурной рекурсии.
И тут мы приходим... к классической проблеме останова.
> и показываю, что на таком-то вот шаге выполняется условие останова
Это невозможно сделать в общем случае.
Счетным и конечным. Счетным-то оно является и в теоретическом брейнфаке с бесконечной памятью.
- НРЗБ
The implementation may assume that any thread will eventually do one of the following:
— terminate,
— make a call to a library I/O function,
— access or modify a volatile object, or
— perform a synchronization operation or an atomic operation.
> если я в одну и туж переменную сечю одно и тоже
Значит это не well-formed программа и её поведение не описывается данным стандартом.
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1528.htm
Но конпелятор особо не понимает, что там происходит. Он просто менее агрессивно оптимизирует вокруг таких участков.
Т.е. например если ты обращаешься к атомику с семантикой aquire (внутри взятия лочки обычно такой и есть), то конпелятор не может переставить какие-то операции назад через эту границу (тем самым вытащив их из-под лочки).
См. https://govnokod.ru/26983.