1. Куча / Говнокод #26981

    +2

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    15. 15
    16. 16
    17. 17
    18. 18
    19. 19
    20. 20
    21. 21
    22. 22
    23. 23
    24. 24
    25. 25
    26. 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).

    https://codecs.multimedia.cx/2020/09/why-rust-is-not-a-mature-programming-language/

    Запостил: 3.14159265, 27 Сентября 2020

    Комментарии (62) RSS

    • Квалифицированный разбор пuтушатни.
      Ответить
    • > because there’s no formal specification to tell you even that much
      То есть в спецификации языка, про которую numухи с гордо раздутыми щеками numушились, что, мол, они ма-те-ма-ти-чес-ки доказали её корректность, попросту отсутствуют настолько важные детали? Блядь, они там ма-те-ма-ти-чес-ки доказывали корректность макроса «println!» что ли?

      Ну да, охуенный способ «убрать» UB: неопределённые кейсы просто не будем включать в спецификацию. Смекалочка!
      Ответить
      • > охуенный способ «убрать» 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).
        И никаких альтернативных компиляторов, как это принято в открытых системах. Одна пропаганда.
        Ответить
        • #скрылвореции
          Ответить
        • > Но статья утверждает никакой формальной спецификации rust вообще не существует!

          Какая спецификация, лол. Первые версии раста, емнип, вообще были что-то типа окамла с иммутабельностью и гц, и что из этого вышло.
          Ответить
          • Получается вся «Ржавчина» — НЕдокументированное UBожище, т.к. существуют разные версии референсного компилятора, зачастую не совместимые между собой.

            И в ней отсутствует чёткая спецификация. Точнее спекой раста является постоянно меняющаяся референсная реализация, основанная на крестовой платформе (!) с кучей своих багров.

            > Первые версии раста, емнип, вообще были что-то типа окамла с иммутабельностью и гц
            Это ещё можно как-то списать на детские болезни, бета-релизы.

            Оно и понятно, ведь спецификации пишут только древние сишники, мерзкие крестобляди и прочие скучные джависты. Нормальному языку спецификация как телеге пятое колесо.
            Ответить
      • > они там ма-те-ма-ти-чес-ки доказывали корректность макроса «println!»

        Зацени ещё вот это.
        Ма-те-ма-ти-чес-ки доказали корректность. Но не в терминах С++.

        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.


        И тут мы приходим к тому, о чём я уже говорил...
        Ответить
        • Что-то не скрывается.

          #скрылвореции
          Ответить
        • Как вообще можно что-то формально доказать, если ты депендишься на сотни(!) мегабайт кода на крестах? Там поди поведение самого конпелятора rust'а то не определено, не то что собранной им программы.
          Ответить
    • My "favourite" recent compiler bug comes from Rust. Compile the following code in Release mode:
      fn main() { (|| loop {})() }

      This defines an anonymous function containing an infinite loop, and calls it. Any sane compiler would make this just loop forever, right?
      $ cargo run --release test
          Illegal instruction (core dumped)
      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
          Ответить
        • >пустой бесконечный цикл?
          void reset() 
          {
            ASSERT(isWatchdogEnabled);
            while (1) ;
          }
          Ответить
      • > definitely not true in Rust

        Где можно прочитать об этом в спеке?

        Нет способа завершить такой цикл не выходя за рамки языка. Тред, который дойдёт до этого цикла, гарантированно никогда не завершится. Именно поэтому шланг подумал, что этот код недостижим и воткнул туда ud2.

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

        > знает что делает

        Тогда он бы добавил в цикл hlt или wfi. Какое-нибудь sha256() в конце-концов, если ему проц погреть хотелось.
        Ответить
        • > Какое-нибудь 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
                Почему, кстати? Питуринговая полнота разве не про вычислимые функции?
                Ответить
                • Возможно аксиома индукции сломается? Это же она делает язык неполным. Хотя я в этом не шарю, конечно.
                  Ответить
                • В Тьюринг-полном языке можно создать терм любого типа с помощью бесконечной рекурсии, к примеру: https://ideone.com/F0lBd5

                  В логике Coq False ­— тип без конструкторов, который играет огромную роль. Термы этого типа не существуют, и поэтому с их помощью можно определить логическое НЕ: "not A := A -> False" (Из A следует несуществующая херь, поэтому A — несуществующая херь). Поэтому любая дыра, позволяющая создать терм с типом False — это мгновенный пиздец любой непротиворечивости.
                  Ответить
                  • P.S. Поправил пример более наглядно: https://ideone.com/F0lBd5
                    Ответить
                  • Т.е. если в проге на расте может существовать пустой бесконечный цикл, то мы можем доказать о ней всё что угодно? Заебись.

                    Походу в крестах его не просто так в UB'ы записали.
                    Ответить
                    • > Т.е. если в расте может существовать пустой бесконечный цикл, то мы можем доказать о коде на расте всё что угодно?

                      Скорее, что доказывать что-либо _на_ расте (а не _о_ нём) — очень плохая идея. Что можно доказать _о_ языке с такими циклами, вопрос сложный, ответ я не знаю.
                      Ответить
                      • P.S. Поэтому, всегда когда видите статьи на помойках типа швабра/медиума про advanced type level programming на Haskell или Scala, и про то, что кто-то с его помощью что-то там доказал, смейтесь им в лицо и тыкайте носом в https://ideone.com/6jyyBW Типы в Тьюринг-полных языках внутренно противоречивы.
                        Ответить
                  • Крайне интересно.
                    Ответить
                  • Понятно, спасибо.
                    А нужна ли для питуринговой полноты бесконечная рекурсия? Она же не нужна для вычисления какой-либо вычислимой функции. Так что в теории, как я вижу, можно иметь питуринг-полный язык, в котором невозможен вечный цикл. А вот как его сделать и не напороться на проблему останова — хз.
                    Ответить
                    • > А нужна ли для питуринговой полноты бесконечная рекурсия?

                      Рекурсии в Тьюринг-полном языке в принципе может не быть (в нём может не быть функций, к примеру), но должен быть тот или иной способ создать программу, которая никогда не завершится. Все Тьюринг-полные языки должны быть эквивалентны, т.е. на любом ТП языке можно написать интерпретатор другого ТП языка. И если брейнфак умеет виснуть, то и хост язык тоже должен это уметь.
                      Ответить
              • >Обходных вариантов много. Можешь описать операционную семантику брейнфака, написать функцию, которая делает один шаг интерпретатора, и экстрагировать её в ocaml

                Каким образом так получается, что на Coq можно написать функцию, делающую один шаг интерпретатора, но сам интерпретатор написать нельзя? По-моему это хуйня какая-то. Ну вот допустим я доказываю теорему про программу на брейнфаке, мне надо доказать, что вполне конкретная брейнфак-программа всегда завершится на каком-то шаге. Что я делаю - я просто N раз применяю функцию "сделай-один-шаг", ну типа step( step(.... step(step(step(step(BF_INITIAL_STATE))) ...)) и показываю, что на таком-то вот шаге выполняется условие останова. Интерпретировать пошагово для доказывания некоторой хуйни вполне можно, значит интерпретатор есть, и написать его можно.
                Ответить
                • > Каким образом так получается, что на Coq можно написать функцию, делающую один шаг интерпретатора, но сам интерпретатор написать нельзя?
                  Как я понял, потому что на коке нельзя написать функцию, которая никогда не завершится. То есть выполнить «+[[>+]>[+>]+]» — полностью валидную программу на «Brainfuck» — не получится. Из этого же следует, что кок не полон по Питурингу.

                  > я просто N раз применяю функцию "сделай-один-шаг"
                  Этим ты докажешь только то, что за N шагов указанная программа либо завершится, либо нет. Провал доказательства не будет обозначать ровным счётом ничего (программа может как никогда не завершиться, так и просто закончиться через N + 1 шагов).
                  Ответить
                • > интерпретировать пошагово

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

                  Для произвольной программы на брейнфаке ты этого доказать, само собой, не можешь. Но для какого-то подмножества программ, наверное, можно.
                  Ответить
                  • > Только если ты можешь доказать, что каждый шаг приближает тебя к остановке. Если не можешь - такой интерпретатор тупо не сконпелируется.

                    Ну так можно написать стратегию на какой-нибудь вспомогательной питушне для Coq, которая будет до усрачки применять интерпретатор к стейту брейнфак-машины, пытаясь дойти до состояния останова, и такая стратегия в процессе своей работы вполне может зависнуть. И вот она уже будет полной по Тьюрингу, осталось только найти компьютер с бесконечной оперативкой, на которой такая стратегия может реально вечно работать
                    Ответить
                • > Каким образом так получается, что на Coq можно написать функцию, делающую один шаг интерпретатора, но сам интерпретатор написать нельзя? По-моему это хуйня какая-то.

                  Coq требует, чтобы все функции были тотальными, т.е. для каждого набора аргументов был результат. Тьюринг-полные языки (включая brainfuck) фундаментально не тотальны, т.к. умеют бесконечно зацикливаться и не возвращать ничего.

                  Один шаг интерпретатора брейнфака можно представить как тотальную чистую функцию: (память, IP, IO buffers) -> (память, IP, IO buffers). С этим проблем нет. Но чтобы выполнить N шагов интерпретатора, тебе нужно _заранее_ знать N, чтобы передавать его в цикл интерпретатора на Gallina. Потому что в Gallina рекурсия обязана делать паттерн-матчинг на каком-то одном аргументе функции, и рекуррентно вызываться только для полученных из него подтермах (выше я постарался объяснить почему). В общем случае такого N нет.
                  Ответить
                  • А если я возьму какое-то подмножество программ? Например:

                    - цикл должен перед ] возвращать курсор в то же место, где он был при [
                    - цикл должен монотонно уменьшать или увеличивать свою ячейку на 1
                    - цикл не должен менять ячейки, которые находятся слева

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

                    Я смогу сказать, что мой интерпретатор существует только для такого подмножества? Ну и дальше пусть вызывающий код доказывает, что прога действительно подчиняется этим правилам.
                    Ответить
                    • > Поскольку код конечен, любая такая прога сможет завершиться.

                      И назвать новый язык Total brainfuck. Можно ещё разрешить бесконечные циклы, которые гарантированно делают I/O, и запилить интерпретатор на корекурсии. С её помощью в gallina можно бесконечно зацикливаться, но только если ты на каждой итерации _приделывашь_ к структурному аргументу новый конструктор, т.е. выполняешь процесс, обратный структурной рекурсии.
                      Ответить
                • > я просто N раз применяю функцию "сделай-один-шаг", ну типа step( step(.... step(step(step(step(BF_INITIAL_STATE))) ...))

                  И тут мы приходим... к классической проблеме останова.

                  > и показываю, что на таком-то вот шаге выполняется условие останова
                  Это невозможно сделать в общем случае.
                  Ответить
                  • проблема тут еще в том, что классической проблемы останова в реальном мире не существует, она есть только в головах теоретиков. Потому что в реальной ЭВМ у нас всегда есть конечный объем оперативной памяти, регистров процессора и НЖМД. А тот же брейнфак на реальном компьютере написать в принципе нельзя, потому как ему нужна бесконечная лента под оперативную память. Если же мы будем рассматривать брейнфак, где оперативка каким-то образом ограничена (например зациклена как кольцевой буфер, или если залазить слишком далеко то происходит останов) то такой реальный брейнфак внезапно оказывается вполне разрешимым, потому как множество всех его состояний является счетным, любое зависание для такого брейнфака является доказуемым, ведь состояние при зависании обязательно повторится, и тут можно применить https://ru.wikipedia.org/wiki/Нахождение_цикла
                    Ответить
                    • > потому как множество всех его состояний является счетным

                      Счетным и конечным. Счетным-то оно является и в теоретическом брейнфаке с бесконечной памятью.
                      Ответить
                    • > НЖМД
                      - НРЗБ
                      Ответить
                      • Ой, ты может еще и ОЗУ не знаешь, что такое? И ПЗУ? и НГМД?
                        Ответить
          • P.S. Никаких хитрых эвристик в termination checker'е, насколько я знаю, нет. Кроме того, что иногда он сам умеет находить структурный аргумент, а иногда ему надо подсказывать (Fixpoint foo a b c {struct a} := ...).
            Ответить
      • показать все, что скрытоvanished
        Ответить
        • "PHP".
          Ответить
        • 1.10 Multi-threaded executions and data races

          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 программа и её поведение не описывается данным стандартом.
          Ответить
          • показать все, что скрытоvanished
            Ответить
            • Для оптимизаций, как обычно.
              http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1528.htm
              // As N1509 correctly points out, the current draft essentially gives undefined
              // behavior to infinite loops in 6.8.5p6. A major issue for doing so is that it
              // allows code to move across a potentially non-terminating loop. For example,
              // assume we have the following loops, where count and count2 are global variables
              // (or have had their address taken), and p is a local variable, whose address has
              // not been taken:
              
              for (p = q; p != 0; p = p -> next) {
                  ++count;
              }
              for (p = q; p != 0; p = p -> next) {
                  ++count2;
              }
              
              // Could these two loops be merged and replaced by the following loop?
              
              for (p = q; p != 0; p = p -> next) {
                      ++count;
                      ++count2;
              }
              
              // Without the special dispensation in 6.8.5p6 for infinite loops, this would be disallowed:
              // If the first loop doesn't terminate because q points to a circular list, the original
              // never writes to count2. Thus it could be run in parallel with another thread that
              // accesses or updates count2. This is no longer safe with the transformed version which
              // does access count2 in spite of the infinite loop. Thus the transformation potentially
              // introduces a data race.
              Ответить
              • показать все, что скрытоvanished
                Ответить
                • Даже более того: встретив такой цикл, конпелятор может сделать что угодно. Хоть int3 впилить на его место.
                  Ответить
                  • показать все, что скрытоvanished
                    Ответить
                    • Ещё нужно учитывать кучу вредных мелочей, в частности, многопоточных.
                      int p = 0;
                      int *q = nullptr;
                      
                      void f() {
                           if (p == 0) {
                              while (p == 0) { /* ... */ }  // Потенциально конечный
                          }
                      
                          int i = 0;
                          q = &i;
                          while (i == 0) { /* ... */ }  // Потенциально конечный, хотя в условии только автоматическая пельменная
                      }
                      Ответить
                      • показать все, что скрытоvanished
                        Ответить
                        • Соседний поток не может трогать твою переменную по ссылке, если она не атомик, не волатайл и не под лочкой. Это data race, которых не бывает в well-defined программе. И если бы что-то из этого у тебя в коде было - компилятор не выбросил бы цикл.
                          Ответить
                          • показать все, что скрытоvanished
                            Ответить
                            • В реализации лочки будет или вызов или атомик, да.

                              Но конпелятор особо не понимает, что там происходит. Он просто менее агрессивно оптимизирует вокруг таких участков.

                              Т.е. например если ты обращаешься к атомику с семантикой aquire (внутри взятия лочки обычно такой и есть), то конпелятор не может переставить какие-то операции назад через эту границу (тем самым вытащив их из-под лочки).
                              Ответить
                          • И даже глобальную пельменную не может? Охуеть.
                            См. https://govnokod.ru/26983.
                            Ответить

    Добавить комментарий