• Test post of formatting of execution trace

    From olcott@21:1/5 to olcott on Wed Mar 3 11:48:03 2021
    On 3/3/2021 11:44 AM, olcott wrote:
    #include <stdint.h>
    #define u8 uint8_t
    #define u32 uint32_t
    #define u16 uint16_t

    u32 Halts(u32 P, u32 I)
    {
      ((void(*)(int))P)(I);
      return 1;
    }



    // P has the machine address of H_Hat()
    void H_Hat(u32 P)
    {
      u32 Input_Halts = Halts(P, P);
      if (Input_Halts)
        HERE: goto HERE;
      return;
    }


    int main()
    {
      u32 Input_Would_Halt = Halts((u32)H_Hat, (u32)H_Hat);
      Output("Input_Would_Halt = ", Input_Would_Halt);
    }

    Because the execution trace shown below shows that H_Hat() invokes
    Halts() with the same data two times in sequence we can conclude that
    H_Hat() is invoked in infinite recursion entirely based on the execution trace of H_Hat() and the assumption that Halts() does nothing besides
    execute or emulate its input.

    When Halts() is augmented so that it can see that H_Hat() invokes it two times in sequence with the same data then Halts() can determine that
    H_Hat() is infinitely recursive.

    _Halts()
    [000004af](01) 55 push ebp
    [000004b0](02) 8bec mov ebp,esp
    [000004b2](03) 8b450c mov eax,[ebp+0c]
    [000004b5](01) 50 push eax
    [000004b6](03) ff5508 call dword [ebp+08]
    [000004b9](03) 83c404 add esp,+04
    [000004bc](05) b801000000 mov eax,00000001
    [000004c1](01) 5d pop ebp
    [000004c2](01) c3 ret

    _H_Hat()
    [0000088f](01) 55 push ebp
    [00000890](02) 8bec mov ebp,esp
    [00000892](01) 51 push ecx
    [00000893](03) 8b4508 mov eax,[ebp+08]
    [00000896](01) 50 push eax ; 2nd Param
    [00000897](03) 8b4d08 mov ecx,[ebp+08]
    [0000089a](01) 51 push ecx ; 1st Param
    [0000089b](05) e80ffcffff call 000004af ; Halts(P,P)
    [000008a0](03) 83c408 add esp,+08
    [000008a3](03) 8945fc mov [ebp-04],eax
    [000008a6](04) 837dfc00 cmp dword [ebp-04],+00
    [000008aa](02) 7402 jz 000008ae
    [000008ac](02) ebfe jmp 000008ac
    [000008ae](02) 8be5 mov esp,ebp
    [000008b0](01) 5d pop ebp
    [000008b1](01) c3 ret

    _main()
    [000008bf](01) 55 push ebp
    [000008c0](02) 8bec mov ebp,esp
    [000008c2](01) 51 push ecx
    [000008c3](05) 688f080000 push 0000088f
    [000008c8](05) 688f080000 push 0000088f
    [000008cd](05) e8ddfbffff call 000004af
    [000008d2](03) 83c408 add esp,+08
    [000008d5](03) 8945fc mov [ebp-04],eax
    [000008d8](03) 8b45fc mov eax,[ebp-04]
    [000008db](01) 50 push eax
    [000008dc](05) 680b030000 push 0000030b
    [000008e1](05) e869faffff call 0000034f
    [000008e6](03) 83c408 add esp,+08
    [000008e9](02) 33c0 xor eax,eax
    [000008eb](02) 8be5 mov esp,ebp
    [000008ed](01) 5d pop ebp
    [000008ee](01) c3 ret

    Push instructions have already pushed the value shown in their in the
    third column. The two push instructions preceding the call to Simulate()
    are its second and first parameters respectively.

    Columns
    (1) Machine address of instruction
    (2) Machine address of top of stack
    (3) Value of top of stack after instruction executed
    (4) Assembly language text


    Columns
    (1) Machine address of instruction
    (2) Machine address of top of stack
    (3) Value of top of stack after instruction executed
    (4) Assembly language text
    [000008bf][00011208][00000000] push ebp
    [000008c0][00011208][00000000] mov ebp,esp
    [000008c2][00011204][00000000] push ecx
    [000008c3][00011200][0000088f] push 0000088f
    [000008c8][000111fc][0000088f] push 0000088f

    [000008cd][000111f8][000008d2] call 000004af
    [0000088f][000111e8][000111f4] push ebp
    [00000890][000111e8][000111f4] mov ebp,esp
    [00000892][000111e4][00000000] push ecx
    [00000893][000111e4][00000000] mov eax,[ebp+08]
    [00000896][000111e0][0000088f] push eax ; 2nd Param [00000897][000111e0][0000088f] mov ecx,[ebp+08]
    [0000089a][000111dc][0000088f] push ecx ; 1st Param [0000089b][000111d8][000008a0] call 000004af ; Call Halts(88f, 88f);

    [0000088f][000111c8][000111d4] push ebp
    [00000890][000111c8][000111d4] mov ebp,esp
    [00000892][000111c4][0000088f] push ecx
    [00000893][000111c4][0000088f] mov eax,[ebp+08]
    [00000896][000111c0][0000088f] push eax ; 2nd Param [00000897][000111c0][0000088f] mov ecx,[ebp+08]
    [0000089a][000111bc][0000088f] push ecx ;1st Param [0000089b][000111b8][000008a0] call 000004af ;Call Halts(88f, 88f);



    --
    Copyright 2021 Pete Olcott

    "Great spirits have always encountered violent opposition from mediocre
    minds." Einstein

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From olcott@21:1/5 to All on Wed Mar 3 11:44:43 2021
    #include <stdint.h>
    #define u8 uint8_t
    #define u32 uint32_t
    #define u16 uint16_t

    u32 Halts(u32 P, u32 I)
    {
    ((void(*)(int))P)(I);
    return 1;
    }



    // P has the machine address of H_Hat()
    void H_Hat(u32 P)
    {
    u32 Input_Halts = Halts(P, P);
    if (Input_Halts)
    HERE: goto HERE;
    return;
    }


    int main()
    {
    u32 Input_Would_Halt = Halts((u32)H_Hat, (u32)H_Hat);
    Output("Input_Would_Halt = ", Input_Would_Halt);
    }

    Because the execution trace shown below shows that H_Hat() invokes
    Halts() with the same data two times in sequence we can conclude that
    H_Hat() is invoked in infinite recursion entirely based on the execution
    trace of H_Hat() and the assumption that Halts() does nothing besides
    execute or emulate its input.

    When Halts() is augmented so that it can see that H_Hat() invokes it two
    times in sequence with the same data then Halts() can determine that
    H_Hat() is infinitely recursive.

    _Halts()
    [000004af](01) 55 push ebp
    [000004b0](02) 8bec mov ebp,esp
    [000004b2](03) 8b450c mov eax,[ebp+0c]
    [000004b5](01) 50 push eax
    [000004b6](03) ff5508 call dword [ebp+08]
    [000004b9](03) 83c404 add esp,+04
    [000004bc](05) b801000000 mov eax,00000001
    [000004c1](01) 5d pop ebp
    [000004c2](01) c3 ret

    _H_Hat()
    [0000088f](01) 55 push ebp
    [00000890](02) 8bec mov ebp,esp
    [00000892](01) 51 push ecx
    [00000893](03) 8b4508 mov eax,[ebp+08]
    [00000896](01) 50 push eax ; 2nd Param
    [00000897](03) 8b4d08 mov ecx,[ebp+08]
    [0000089a](01) 51 push ecx ; 1st Param
    [0000089b](05) e80ffcffff call 000004af ; Halts(P,P)
    [000008a0](03) 83c408 add esp,+08
    [000008a3](03) 8945fc mov [ebp-04],eax
    [000008a6](04) 837dfc00 cmp dword [ebp-04],+00
    [000008aa](02) 7402 jz 000008ae
    [000008ac](02) ebfe jmp 000008ac
    [000008ae](02) 8be5 mov esp,ebp
    [000008b0](01) 5d pop ebp
    [000008b1](01) c3 ret

    _main()
    [000008bf](01) 55 push ebp
    [000008c0](02) 8bec mov ebp,esp
    [000008c2](01) 51 push ecx
    [000008c3](05) 688f080000 push 0000088f
    [000008c8](05) 688f080000 push 0000088f
    [000008cd](05) e8ddfbffff call 000004af
    [000008d2](03) 83c408 add esp,+08
    [000008d5](03) 8945fc mov [ebp-04],eax
    [000008d8](03) 8b45fc mov eax,[ebp-04]
    [000008db](01) 50 push eax
    [000008dc](05) 680b030000 push 0000030b
    [000008e1](05) e869faffff call 0000034f
    [000008e6](03) 83c408 add esp,+08
    [000008e9](02) 33c0 xor eax,eax
    [000008eb](02) 8be5 mov esp,ebp
    [000008ed](01) 5d pop ebp
    [000008ee](01) c3 ret

    Push instructions have already pushed the value shown in their in the
    third column. The two push instructions preceding the call to Simulate()
    are its second and first parameters respectively.

    Columns
    (1) Machine address of instruction
    (2) Machine address of top of stack
    (3) Value of top of stack after instruction executed
    (4) Assembly language text
    [000008bf][00011208][00000000] push ebp
    [000008c0][00011208][00000000] mov ebp,esp
    [000008c2][00011204][00000000] push ecx
    [000008c3][00011200][0000088f] push 0000088f
    [000008c8][000111fc][0000088f] push 0000088f

    [000008cd][000111f8][000008d2] call 000004af
    [0000088f][000111e8][000111f4] push ebp
    [00000890][000111e8][000111f4] mov ebp,esp
    [00000892][000111e4][00000000] push ecx
    [00000893][000111e4][00000000] mov eax,[ebp+08]
    [00000896][000111e0][0000088f] push eax ; 2nd Param [00000897][000111e0][0000088f] mov ecx,[ebp+08]
    [0000089a][000111dc][0000088f] push ecx ; 1st Param [0000089b][000111d8][000008a0] call 000004af ; Call Halts(88f, 88f);

    [0000088f][000111c8][000111d4] push ebp
    [00000890][000111c8][000111d4] mov ebp,esp
    [00000892][000111c4][0000088f] push ecx
    [00000893][000111c4][0000088f] mov eax,[ebp+08]
    [00000896][000111c0][0000088f] push eax ; 2nd Param [00000897][000111c0][0000088f] mov ecx,[ebp+08]
    [0000089a][000111bc][0000088f] push ecx ;1st Param ...[0000089b][000111b8][000008a0] call 000004af ;Call Halts(88f, 88f);

    It continues to execute the same portion of H_Hat() sequence above


    --
    Copyright 2021 Pete Olcott

    "Great spirits have always encountered violent opposition from mediocre
    minds." Einstein

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)