diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 0000000..9ee1e25 --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,22 @@ +name: Build + +on: [ push, pull_request ] + +jobs: + build: + name: Build + runs-on: windows-latest + + steps: + - uses: actions/checkout@v3 + - uses: stevenwdv/setup-fasm@v1 + with: + edition: fasm1 + - run: fasm asmsequent.asm + env: + inc: ${{ env.INCLUDE }} + - uses: actions/upload-artifact@v3 + with: + name: asmsequent.exe + path: asmsequent.exe + if-no-files-found: error diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..ea5e51c --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +*.exe +*.fas +*.o diff --git a/README.md b/README.md new file mode 100644 index 0000000..4dbb548 --- /dev/null +++ b/README.md @@ -0,0 +1,27 @@ +Assembly sequent solver GUI +=========================== + +Solves a [sequent](https://en.wikipedia.org/wiki/Sequent) you enter by [applying rules](https://en.wikipedia.org/wiki/Sequent_calculus) and displays the resulting [tableau](https://en.wikipedia.org/wiki/Method_of_analytic_tableaux). +A sequent is open if the propositional formula to the left of the `@` can be true while simultaneously the formula on the right is false, in this case the program displays the list of possible valuations with true variables to the left of a bar (`|`) and false variables to the right (the valuations may include duplicates). A sequent is closed if this is not satisfiable. +Hence, you can use `φ @` for some propositional formula `φ` to check if `φ` is satisfiable, and you can use `@ φ` to check if the negation is unsatisfiable to check if `φ` is always true. + +This is just a program I made for fun during a course in 2018 (my first large assembly program). +It's not (made to be) particularly efficient, since it allocates all terms on the heap to display the tableau later. Most of the running time is actually spent on concatenating strings to display it. However, it should work correctly, be crash-free (if it has enough memory), and not have memory leaks. Although it doesn't always check if Windows/MSVC functions it calls return success. + +This was written for [flat assembler](https://flatassembler.net/) 1. Point the `inc` environment variable to the fasm `INCLUDE` directory when building. You can also open the `.fpr` project file with the [Fresh IDE](https://fresh.flatassembler.net/). In Fresh, you can set `inc` as an 'alias' via the IDE/project options. + +It works on x86-64 Windows and on Linux with Wine. + +The assembly files in the initial commit are the original ones from 2018, so they still contain some TODOs for stuff that could be done and some commented/unused legacy code. + +Credit me with a [link to the repository](https://github.com/stevenwdv/asmsequent) if you use this somewhere for some reason! + +Screenshots +----------- + +![Closed](screenshots/closed.png) +`a & b` cannot be true while `a | b` is false. + +![Open: tableau](screenshots/open-tableau.png "idk?") +![Open: valuations](screenshots/open-valuations.png) +`c -> a & b` is true if either `c` is false or `a` and `b` are both true. diff --git a/asmsequent.asm b/asmsequent.asm new file mode 100644 index 0000000..ba49861 --- /dev/null +++ b/asmsequent.asm @@ -0,0 +1,724 @@ +format PE64 GUI +entry start + +;TODO use 32b e.x more often + +;make fbound insert bounds +DEBUGBOUND = FALSE +;enable console and deb* +DEBUGSTR = FALSE +;print allocations etc (requires DEBUGSTR) +DEBUGMEM = FALSE + +;norm/adv +PRINTMODE = 0 + +include '%inc%\win64a.inc' + +include 'proc_mod.inc' +include 'memory.inc' + +macro rpop [arg] {reverse pop arg} + +macro fbound { +if DEBUGBOUND + nop + times 8 int3 + nop +end if + align 16 +} + +macro debs s* { +if DEBUGSTR + save_inline rax, rcx, rdx, r8, r9, r10, r11 +; cinvoke puts, s + cinvoke fputs, s, [stdout] + cinvoke fputc, 10, [stdout] + cinvoke flushall + rest +end if +} +macro debi i* { +if DEBUGSTR + save_inline rax, rcx, rdx, r8, r9, r10, r11 +; cinvoke printf, s_debug_udec, i + cinvoke fprintf, [stdout], s_debug_udec, i + cinvoke flushall + rest +end if +} +macro debx i* { +if DEBUGSTR + save_inline rax, rcx, rdx, r8, r9, r10, r11 +; cinvoke printf, s_debug_hex, i + cinvoke fprintf, [stdout], s_debug_hex, i + cinvoke flushall + rest +end if +} + + +;Tab control item +struct TCITEM + mask rd 1 + dwState rd 1 + dwStateMask rd 2 ;2 because of padding, probably due to alignment + pszText rq 1 + cchTextMax rd 1 + iImage rd 1 + lParam rd 1 +ends + + +arg1 equ rcx +arg2 equ rdx +arg3 equ r8 +arg4 equ r9 + +NEWL equ 13,10 + +;===================================== +section '.data' data readable writable +;===================================== + +if DEBUGSTR +s_debug_udec db "%llu",10,0 +s_debug_hex db "%#llx",10,0 +end if + +if DEBUGMEM +s_malloc db "+",0 +s_realloc db "*%#llx",10,"+",0 +s_free db "-%#llx",10,0 +end if + +s_newline db NEWL,0 +s_space db " ",0 +s_err db "Error",0 +s_err_tside db "Error on true side",0 +s_err_fside db "Error on false side",0 + +s_e_no_sep db "No @ separator seen",0 +s_e_multiple_sep db "Multiple @ separators seen",0 +s_e_sep dq s_e_no_sep, s_e_multiple_sep + +s_state_closed db "Closed (always false)",0 +s_state_open db "Open (can be true)",0 +s_states dq s_state_closed, s_state_open + +s_tableau db "Tableau",0 +s_valuations db "Valuations",0 + +align 8 + +_heap rq 1 + +term_t_actions_jmp dq t_actions.not, t_actions.and, t_actions.or, t_actions.imp, t_actions.eqv +term_f_actions_jmp dq f_actions.not, f_actions.and, f_actions.or, f_actions.imp, f_actions.eqv + +stdout rq 1 + +hDlg rq 1 +hInput rq 1 +hState rq 1 +hTabs rq 1 + +hOutput rq 1 +hValuations rq 1 + +tabTableau TCITEM TCIF_TEXT,,,s_tableau,,, +tabValuations TCITEM TCIF_TEXT,,,s_valuations,,, + + +include 'print_strings.inc' +include 'parse_strings.inc' + + +;======================================= +section '.code' code readable executable +;======================================= + +include 'sequent.inc' +include 'term.inc' +include 'print.inc' +include 'tokens.inc' +include 'parse.inc' +include 'term_actions.inc' + + +;hdlg, msg, wparam, lparam +fbound +dlg_proc: + save_nothing + + cmp arg2, WM_NOTIFY + je .notify + + cmp arg2, WM_COMMAND + je .command + + cmp arg2, WM_INITDIALOG + je .init + + cmp arg2, WM_CLOSE + je .close + + jmp .not_processed + + .notify: + cmp arg3, ID_TABS + je .switch_tab + + jmp .not_processed + + .switch_tab: + invoke SendMessage, [hTabs], TCM_GETCURSEL, NULL, NULL + + save_inline rax + invoke ShowWindow, [hOutput+rax*8], SW_SHOW + rest + + neg rax + inc rax + invoke ShowWindow, [hOutput+rax*8], SW_HIDE + + jmp .processed + + .command: + cmp arg3, BN_CLICKED shl 16 + ID_DOITBTN + je .solve + + jmp .not_processed + + .solve: + ccall solve + jmp .processed + + .init: + mov [hDlg], arg1 + + invoke GetDlgItem, arg1, ID_INPUT + mov [hInput], rax + + invoke GetDlgItem, [hDlg], ID_OUTPUT + mov [hOutput], rax + + invoke GetDlgItem, [hDlg], ID_STATE + mov [hState], rax + + invoke GetDlgItem, [hDlg], ID_TABS + mov [hTabs], rax + + invoke GetDlgItem, [hDlg], ID_VALUATIONS + mov [hValuations], rax + + invoke SendMessage, [hTabs], TCM_INSERTITEM, 0, tabTableau + invoke SendMessage, [hTabs], TCM_INSERTITEM, 1, tabValuations + + jmp .processed + + .close: + invoke EndDialog, arg1, NULL + + .processed: + mov rax, TRUE + resti + ret + + .not_processed: + xor eax,eax + rest + ret + + +fbound +start: + save_nothing + + cinvoke GetProcessHeap + mov [_heap], rax + +if DEBUGSTR + invoke AllocConsole + + invoke CreateFile, "CONOUT$", GENERIC_WRITE, 0, NULL, 3, FILE_ATTRIBUTE_NORMAL, NULL + cinvoke open_osfhandle, rax, 1 + cinvoke fdopen, rax, "w" + mov [stdout], rax + +; cinvoke iob_func, 0 +; mov rcx, [stdout] +; mov [rax+8], rcx +; +; cinvoke iob_func, 0 +; add rax, 8 +; cinvoke freopen, "CONOUT$", "w", rax +end if + + debs " ====> starting..." + invoke GetModuleHandle, NULL + invoke DialogBoxParam, eax, 100, HWND_DESKTOP, dlg_proc, NULL + + invoke ExitProcess, 0 + rest + ret + + +;TODO optimize register count? + +;Action when pressing Solve button +fbound +solve: + save r12,r13,r14,r15,rsi,rbx + + ;==== GET INPUT SEQUENT ==== + + invoke GetWindowTextLength, [hInput] + inc rax ;for 0 terminator, may be unnecessary? (TODO) + mov r12, rax ;r12: buflen + + ;allocate buffer + malloc rax + string equ rbx + mov string, rax + + invoke GetWindowText, [hInput], rax, r12 + + ;==== TOKENIZE ==== + + debs " ====> tokenizing..." + + ccall tokenize, string + test rax,rax + jnz .error_tokenize + tokens equ r12 + mov tokens, arg2 + + ;==== GROUP VARIABLES ==== + + debs " ====> grouping..." + ccall tokens_group_vars, string ;, arg2/tokens + vars equ rsi + vars_len equ r15 + mov vars, arg3 + mov vars_len, arg4 + mfree string + + ;==== SPLIT SIDES ==== + + debs " ====> splitting..." + ccall split_sides, tokens + test al,al + jnz .error_split + tokens_fside equ r13 + mov tokens_fside, arg2 + + ;==== PARSE ==== + + ;tside + debs " ====> parsing tside..." + ccall parse, tokens + term_tside equ r14 + test rax,rax + jnz .error_parse_tside + mov term_tside, arg1 + + ;fside + debs " ====> parsing fside..." + ccall parse, tokens_fside + restore tokens_fside + term_fside equ r13 + test rax,rax + jnz .error_parse_fside + mov term_fside, arg1 + + mfree tokens + + + ;==== PREPARE SEQUENT ==== + + debs " ====> allocating sequent..." + + malloc sizeof.SEQUENT_STATE + mov [rax+SEQUENT.child1], NULL + mov [rax+SEQUENT.child2], NULL + sequent equ r12 + mov sequent, rax + + macro alloc_side sidepre* { + local ..empty, ..done + + test term_#sidepre#side,term_#sidepre#side + jz ..empty + + malloc 8 + mov [sequent+SEQUENT.#sidepre#side], rax + mov [sequent+SEQUENT.#sidepre#len], 1 + mov [rax], term_#sidepre#side + jmp ..done + + ..empty: + malloc 0 + mov [sequent+SEQUENT.#sidepre#side], rax + mov [sequent+SEQUENT.#sidepre#len], 0 + + ..done: + } + + alloc_side t + alloc_side f + purge alloc_side + + + ;==== SOLVE ==== + + debs " ====> solving..." + ccall seq_solve, sequent, NULL + ;mov sequent, arg1 + + + ;==== PRINT SOLUTION ==== + + debs " ====> printing solution..." + + invoke SetWindowText, [hState], [s_states+rax*8] + + + ;allocate buffer + malloc 4096 + sub rsp, 8 + push 4096 + push 0 + push rax + + mov arg1, rsp + frame + ccall print_seq, , sequent, 0 + endf + + buf equ r14 + buflen equ r13 + pop buf + pop buflen + add rsp, $10 + + ;append 0 terminator + inc buflen + realloc buf, buflen + mov buf, rax + mov byte[rax+buflen-1], 0 + + invoke SetWindowText, [hOutput], rax + mfree buf + restore buf,buflen + + + debs " ====> printing valuations..." + invoke SendMessage, [hValuations], LB_RESETCONTENT, NULL, NULL + ccall add_valuations, sequent + + + ;==== FREE ==== + + debs " ====> freeing resources..." + + cmp [sequent+SEQUENT.tlen], 0 + jz @f + + mov rax, [sequent+SEQUENT.tside] + ccall term_free, qword[rax] + @@: + + cmp [sequent+SEQUENT.flen], 0 + jz @f + + mov rax, [sequent+SEQUENT.fside] + ccall term_free, qword[rax] + @@: + + ccall seq_free, sequent + + ccall free_variables, vars, vars_len + + resti + ret + + +.error_tokenize: + mov r12, rax + mfree string + invoke MessageBox, [hDlg], r12, s_err, MB_ICONERROR+MB_OK + mfree r12 + resti + ret + +.error_split: + mov r13, rax + mfree tokens + ccall free_variables, vars, vars_len + invoke MessageBox, [hDlg], [s_e_sep + 8*(r13-split_sides.ERR_NO_SEP)], s_err, MB_ICONERROR+MB_OK + resti + ret + +.error_parse_tside: + mov r13, rax + mfree tokens + ccall free_variables, vars, vars_len + invoke MessageBox, [hDlg], r13, s_err_tside, MB_ICONERROR+MB_OK + mfree r13 + resti + ret + +.error_parse_fside: + mov r13, rax + mfree tokens + + test term_tside,term_tside + jz .error_parse_fside.skip_free + + ccall term_free, term_tside + .error_parse_fside.skip_free: + + ccall free_variables, vars, vars_len + invoke MessageBox, [hDlg], r13, s_err_fside, MB_ICONERROR+MB_OK + mfree r13 + rest + ret + +restore vars,vars_len,sequent,tokens,term_tside,term_fside + + + +sequent equ r12 + +;Add valuations (from open leaf sequents) to hValuations list +;TODO no duplicate vars + no duplicate valuations + +;sequent +fbound +add_valuations: + save r12 + mov sequent, arg1 + + cmp [sequent+SEQUENT.child1], NULL + je .leaf + + ccall add_valuations, [sequent+SEQUENT.child1] + cmp [sequent+SEQUENT.child2], NULL + jne .two_childs + resti + ret + + .two_childs: + ccall add_valuations, [sequent+SEQUENT.child2] + resti + ret + + .leaf: + cmp [sequent+SEQUENT_STATE.state], SEQUENT_OPEN + je .open + resti + ret + + .open: + save_inline rsi,rdi + mov rdx, 3 ;rdx: tot length + + macro add_side prefix* { + local ..loop, ..skip + + mov r8, [sequent+SEQUENT.#prefix#len] + test r8,r8 + jz ..skip + mov rsi, [sequent+SEQUENT.#prefix#side] + align 16 + ..loop: + lodsq + lea rdi, [rax+TERMVAR.t1] + xor eax,eax + or rcx, -1 + repnz scasb + neg rcx + dec rcx ;rcx: var length + 1 for ' ' + + add rdx, rcx + dec r8 + jnz ..loop + ..skip: + } + + add_side t + add_side f + purge add_side + + mov rax, rdx + malloc rax + mov rdi, rax + mov r10, rax + + macro copy_side prefix* { + local ..loop, ..char_loop, ..char_done, ..skip + + mov r8, [sequent+SEQUENT.#prefix#len] + test r8,r8 + jz ..skip + mov r9, [sequent+SEQUENT.#prefix#side] + align 16 + ..loop: + mov rsi, [r9] ;TERMVAR ptr + inc rsi ;skip TERM.type + ..char_loop: + lodsb + test al,al + jz ..char_done + + stosb + jmp ..char_loop + + ..char_done: + mov eax, ' ' + stosb + + add r9, 8 + dec r8 + jnz ..loop + ..skip: + } + + copy_side t + + mov eax, '|' + stosb + mov eax, ' ' + stosb + + copy_side f + + purge copy_side + mov byte[rdi], 0 + + mov rdi, r10 + invoke SendMessage, [hValuations], LB_ADDSTRING, , r10 + mfree rdi + + rest + + rest + ret +restore sequent + + + +;==================================== +section '.idata' import data readable +;==================================== + +library kernel,'kernel32.dll',\ + user,'user32.dll',\ + msvcrt,'msvcrt.dll' + +import kernel,\ + GetProcessHeap,'GetProcessHeap',\ + GetModuleHandle,'GetModuleHandleA',\ + HeapAlloc,'HeapAlloc',\ + HeapReAlloc,'HeapReAlloc',\ + HeapFree,'HeapFree',\ + HeapWalk,'HeapWalk',\ + ExitProcess,'ExitProcess',\ + AllocConsole,'AllocConsole',\ + CreateFile,'CreateFileA',\ + GetTickCount64,'GetTickCount64' + +import user,\ + DialogBoxParam,'DialogBoxParamA',\ + MessageBox,'MessageBoxA',\ + SendMessage,'SendMessageA',\ + GetDlgItem,'GetDlgItem',\ + GetWindowTextLength,'GetWindowTextLengthA',\ + GetWindowText,'GetWindowTextA',\ + SetWindowText,'SetWindowTextA',\ + EndDialog,'EndDialog',\ + ShowWindow,'ShowWindow' + +import msvcrt,\ + vscprintf,'_vscprintf',\ + vsprintf,'vsprintf',\ + fputs,'fputs',\ + fputc,'fputc',\ + getchar,'getchar',\ + fprintf,'fprintf',\ + fdopen,'_fdopen',\ + open_osfhandle,'_open_osfhandle',\ + flushall,'_flushall',\ + printf,'printf',\ + puts,'puts',\ + putchar,'putchar',\ + iob_func,'__iob_func',\ + freopen,'freopen' + + +;===================================== +section '.rsrc' resource data readable +;===================================== + +directory RT_DIALOG, dialogs,\ + RT_MANIFEST, manifests,\ + RT_VERSION, vinfos + + +resource dialogs, 100, LANG_ENGLISH + SUBLANG_DEFAULT, main_dialog + +;CONTROL\s*(".*?[^\\]"|""|'.*?[^\\]'|'')\s*,\s*(\d+?)\s*,\s*(.+?)\s*,\s*(.+?)\s*,\s*(\d+?)\s*,\s*(\d+?)\s*,\s*(\d+?)\s*,\s*(\d+) +; dialogitem "$3", $1, $2, $5,$6,$7,$8, $4 + +ID_INPUT = 101 +ID_OUTPUT = 102 +ID_DOITBTN = 103 +ID_STATE = 104 +ID_TABS = 105 +ID_VALUATIONS = 106 + +NEWL equ ,13,10, + +;" a&b|c->(d<->e)|!f || g&&h" NEWL "@" NEWL " a/\b\/c->(d<->e)\/~f" +;Long: +;a&b|c->(d<->e)<->a&b|c->(d<->e)<->a&b|c->(d<->e) @ a&b|c->(d<->e)->HEYhello<->!!hi&a&b|c->(d<->e)->HEYhello<->!!hi + +dialog main_dialog, "ASM Sequent", 0,0,470,340, DS_CENTER + WS_CAPTION + WS_SYSMENU + WS_MINIMIZEBOX, WS_EX_CLIENTEDGE, , "Consolas",10 + dialogitem "BUTTON", "Input: sequent", -1, 2,0,466,70, BS_GROUPBOX + WS_CHILD + WS_VISIBLE + WS_GROUP + dialogitem "EDIT", " a&b|c->(d<->e)|!f || g&&h" NEWL "@" NEWL " a/\b\/c->(d<->e)\/~f",\ + ID_INPUT, 4,9,463,58, ES_LEFT + ES_MULTILINE + ES_WANTRETURN + WS_CHILD + WS_VISIBLE + WS_BORDER + WS_VSCROLL + WS_HSCROLL + WS_TABSTOP + + dialogitem "SysTabControl32", "", ID_TABS, 1,71,469,237+15, TCS_TABS + TCS_MULTILINE + WS_CHILD + WS_VISIBLE + WS_TABSTOP + + dialogitem "EDIT", "", ID_OUTPUT, 4,86,463,234, ES_LEFT + ES_MULTILINE + ES_READONLY + WS_CHILD + WS_VISIBLE + WS_BORDER + WS_VSCROLL + WS_HSCROLL + WS_TABSTOP + dialogitem "LISTBOX", "", ID_VALUATIONS, 4,86,463,234, LBS_STANDARD + WS_CHILD + WS_TABSTOP + LBS_EXTENDEDSEL + + dialogitem "BUTTON", "Solve!", ID_DOITBTN, 407,324,60,14, BS_PUSHBUTTON + WS_CHILD + WS_VISIBLE + WS_GROUP + WS_TABSTOP + dialogitem "STATIC", "", ID_STATE, 4,327,133,10, SS_LEFT + WS_CHILD + WS_VISIBLE + WS_GROUP +enddialog + + + +resource manifests,\ + 1, LANG_ENGLISH + SUBLANG_DEFAULT, manifest + +resdata manifest +;Use visual styles + db '' + db '' +endres + + +resource vinfos,\ + 1, LANG_ENGLISH + SUBLANG_DEFAULT, vinfo + +COPY equ ,$a9, ;(c) +versioninfo vinfo, VOS__WINDOWS32, VFT_APP, VFT2_UNKNOWN, LANG_ENGLISH + SUBLANG_DEFAULT, 0,\ + 'FileDescription','Assembly sequent solver',\ + 'FileVersion','1.0',\ + 'ProductVersion','1.0',\ + 'ProductName','Assembly sequent solver',\ + 'LegalCopyright','Copyright ' COPY ' Steven WdV' diff --git a/asmsequent.fpr b/asmsequent.fpr new file mode 100644 index 0000000..950263e Binary files /dev/null and b/asmsequent.fpr differ diff --git a/memory.inc b/memory.inc new file mode 100644 index 0000000..5a5bba8 --- /dev/null +++ b/memory.inc @@ -0,0 +1,53 @@ + +;s=`...`.split("\n") +;{const m=[],r=s=>m.splice(m.indexOf(s),1),f={"-":r,"*":r,"+":s=>m.push(s)};for(const l of s)f[l[0]]&&f[l[0]](l.substr(1));m} + +macro malloc size* { +if DEBUGMEM +if size eqtype rax + save_inline size + cinvoke fprintf, [stdout], s_malloc, qword[rsp+20h+8] + cinvoke flushall + rest +else + cinvoke fprintf, [stdout], s_malloc, size + cinvoke flushall +end if +;int3 +end if + cinvoke HeapAlloc,[_heap],HEAP_GENERATE_EXCEPTIONS,size +if DEBUGMEM + debx rax +end if +} + +macro realloc ptr*, size* { +if DEBUGMEM +if size eqtype rax + save_inline size,ptr + cinvoke fprintf, [stdout], s_realloc, qword[rsp+20h] ;size left out + cinvoke flushall + rest +else + save_inline ptr + cinvoke fprintf, [stdout], s_realloc, qword[rsp+20h+8] ;size left out + cinvoke flushall + rest +end if +;int3 +end if + cinvoke HeapReAlloc,[_heap],HEAP_GENERATE_EXCEPTIONS,ptr,size +if DEBUGMEM + debx rax +end if +} + +macro mfree ptr { +if DEBUGMEM + save_inline ptr + cinvoke fprintf, [stdout], s_free, qword[rsp+20h+8] + cinvoke flushall + rest +end if + cinvoke HeapFree,[_heap],HEAP_GENERATE_EXCEPTIONS,ptr +} \ No newline at end of file diff --git a/parse.inc b/parse.inc new file mode 100644 index 0000000..e170832 --- /dev/null +++ b/parse.inc @@ -0,0 +1,294 @@ +;Operator precedence parser + +;▼ mind order STACK<>PTR! +;STACK PTR ACT +;$ $ pop_noconstruct + accept +;$ push +; $ pop +;var pop +; var push +;( ) pop_noconstruct + inc +;( push +; ( push +; ) pop +;! op pop +;! push +; ! push +;stong weak pop +;weak strong push +;Lassoc sameop pop +;Rassoc sameop push + +;(!) +;& L assoc +;| L assoc +;-> R assoc +;<-> L assoc + + +;TODO linux wine reduce '[...] but found [no number]' + +tokens equ rsi +term_stack equ r12 +term_stack_lenb equ r13 + +;Parse tokens for one side +; on success, term = term on that side or NULL and error=0 +; on error, error = malloced error string + +;tokens, term O -> error +fbound +parse: + save rsi,r12,r13,r15 + mov tokens, arg1 + + xor term_stack_lenb,term_stack_lenb + malloc term_stack_lenb + mov term_stack, rax + + sub rsp, 8 + push term_stack_lenb ; =TOKEN_END + + align 16 + .loop: + movzx eax, byte[rsi] + +if FALSE + debs "" + debs "P:" + debi rax + debs "S:" + mov r9, [rsp] + debi r9 +end if + + test al,al + jz .P_end ;P: END + + cmp byte[rsp], TOKEN_END + je .push ;S: END + + cmp al, TOKEN_VAR + je .push ;P: VAR + + cmp byte[rsp], TOKEN_VAR + je .pop ;S: VAR + + cmp al, TOKEN_RPAREN + je .P_rparen ;P: RPAREN + + cmp al, TOKEN_LPAREN + je .push ;P: LPAREN + + cmp al, TOKEN_NOT + je .P_not ;P: NOT + + cmp byte[rsp], TOKEN_NOT + je .S_not ;S: NOT + + cmp al, byte[rsp] + jb .push ;P: strong, S: weak + ja .pop ;P: weak, S: strong + + cmp al, TOKEN_IMP + je .push ;P=S and P: Rassoc + jmp .pop ;P=S and P: Lassoc + + .error_pop: ;r15: type + .unwind_loop: + cmp byte[rsp], TOKEN_END + je .unwind_done + + add rsp, $10 + jmp .unwind_loop + .unwind_done: + shr term_stack_lenb, 3 ;Not actually in bytes anymore.. + mov [rsp], term_stack_lenb + + frame + test term_stack_lenb,term_stack_lenb + jz .term_free_done + mov rsi, term_stack + .term_free_loop: + lodsq + ccall term_free, rax + dec term_stack_lenb + jnz .term_free_loop + + .term_free_done: + mfree term_stack + endf + + pop term_stack_lenb + add rsp, 8 ;pop TOKEN_END + + cmp r15, TOKEN_LPAREN + je .error_lparen + cmp r15, TOKEN_RPAREN + je .error_rparen + + xor eax,eax + cmp r15, TOKEN_AND + setae al + inc rax + + asprintf s_parse_e_pop, rax, [s_tokens+(r15-TOKEN_NOT)*8], term_stack_lenb + mov rax, arg1 + resti + ret + + .error_lparen: + asprintf_noparams s_parse_e_lparen + mov rax, arg1 + resti + ret + + .error_rparen: + asprintf_noparams s_parse_e_rparen + mov rax, arg1 + resti + ret + + .error_stack_multiple: + shr term_stack_lenb, 3 + asprintf s_parse_e_stack_multiple, term_stack_lenb + mov rax, arg1 + resti + ret + + .accept: ;P: END, S: END + add rsp, $10 + + test term_stack_lenb,term_stack_lenb + jz .accept_empty + + mov r15, [term_stack] + mfree term_stack + + cmp term_stack_lenb, 8 + ja .error_stack_multiple + + mov arg1, r15 + xor eax,eax + resti + ret + + .accept_empty: + mfree term_stack + + xor arg1,arg1 + xor eax,eax + rest + ret + + +fbound +.P_end: + cmp byte[rsp], TOKEN_END + je .accept ;P: END, S: END + jmp .pop ;P: END, S: !END + +fbound +.P_rparen: + cmp byte[rsp], TOKEN_LPAREN + jne .pop ;P: RPAREN, S: !LPAREN + ;pop '(' and skip ')' + add rsp, 2*8 ;P: RPAREN, S: LPAREN + inc rsi + jmp .loop + +fbound +.P_not: + inc rsi + sub rsp, 8 + push TOKEN_NOT + jmp .loop + +fbound +.S_not: + cmp al, TOKEN_AND + jb .push ;P: !op, S: NOT + ;cmp al, TOKEN_EQV + ;ja .push + jmp .pop ;P: op, S: NOT + + +fbound +.pop: ;AKA reduce + pop r15 ;type + cmp r15, TOKEN_VAR + jne .pop.operator + + pop r15 ;TERMVAR ptr + add term_stack_lenb, 8 + frame + realloc term_stack, term_stack_lenb + endf + mov term_stack, rax + + mov [term_stack+term_stack_lenb-8], r15 ;add var to stack + jmp .loop + + .pop.operator: + add rsp, 8 + cmp r15, TOKEN_NOT + je .pop.not + + cmp r15, TOKEN_LPAREN + je .error_pop + cmp r15, TOKEN_RPAREN + je .error_pop + + cmp term_stack_lenb, 8*2 + jb .error_pop + + frame + malloc sizeof.TERM + endf + dec r15 ;TERM_NOT-TOKEN_NOT = -1 + mov [rax+TERM.type], r15b + + mov rcx, [term_stack+term_stack_lenb-8*2] + mov [rax+TERM.t1], rcx + mov rcx, [term_stack+term_stack_lenb-8] + mov [rax+TERM.t2], rcx + + ;replace with operator + sub term_stack_lenb, 8 + mov [term_stack+term_stack_lenb-8], rax + jmp .loop + + .pop.not: + cmp term_stack_lenb, 8 + jb .error_pop + + frame + malloc sizeof.TERM1 + endf + mov [rax+TERM.type], TERM_NOT + mov rcx, [term_stack+term_stack_lenb-8] + mov [rax+TERM.t1], rcx + + ;replace with operator + mov [term_stack+term_stack_lenb-8], rax + jmp .loop + + +fbound +.push: ;AKA shift + inc rsi + cmp rax, TOKEN_VAR + jne .push.nvar + + ;P: VAR + lodsq + push rax ;TERMVAR ptr + push TOKEN_VAR + jmp .loop + + .push.nvar: ;P: !VAR + sub rsp, 8 + push rax + jmp .loop + +restore tokens,term_stack,term_stack_len \ No newline at end of file diff --git a/parse_strings.inc b/parse_strings.inc new file mode 100644 index 0000000..a295eab --- /dev/null +++ b/parse_strings.inc @@ -0,0 +1,7 @@ +s_tok_e_unexpected db "Expected '%c' instead of '%c' at index %llu",0 +s_tok_e_unknown db "Illegal token '%c' at index %llu",0 + +s_parse_e_pop db "Tried to reduce %hhu term(s) for operation '%s', but found %hhu",0 +s_parse_e_lparen db "Too few closing parentheses",0 +s_parse_e_rparen db "Too many closing parentheses",0 +s_parse_e_stack_multiple db "%hhu parts have no connecting operator(s)",0 \ No newline at end of file diff --git a/print.inc b/print.inc new file mode 100644 index 0000000..4a57a81 --- /dev/null +++ b/print.inc @@ -0,0 +1,189 @@ +;String buffer +struct BUFFER + buf rq 1 + len rq 1 + alloclen rq 1 +ends + +buf equ rbx ;ptr to BUFFER + +;(Not used) +macro doprintf fmt*, [params] { + common + save_inline r12 + asprintf fmt, params + mov r12, arg1 + doprint r12 + mfree r12 + rest +} + +;TODO make more efficient for additions of 1 or 2 chars? + +;Append len chars of string to buf +macro doprint string*, len* { + local ..buf_realloc, ..buf_skip_realloc + ;invoke GetWindowTextLength, [hOutput] + ;invoke SendMessage, [hOutput], EM_SETSEL, rax, rax + ;invoke SendMessage, [hOutput], EM_REPLACESEL, TRUE, string + + mov rsi, string + + mov rax, [buf+BUFFER.len] + mov rdi, rax + add rax, len + mov [buf+BUFFER.len], rax + cmp rax, [buf+BUFFER.alloclen] + ja ..buf_realloc + + add rdi, [buf+BUFFER.buf] + jmp ..buf_skip_realloc + + ..buf_realloc: + add rax, 4096 + mov [buf+BUFFER.alloclen], rax + realloc [buf+BUFFER.buf], rax + mov [buf+BUFFER.buf], rax + add rdi, rax + + ..buf_skip_realloc: + mov rcx, len + rep movsb + + ;cinvoke fprintf, [stdout], string + ;cinvoke flushall +} + +;See __asprintf +macro asprintf fmt*, [params] { + common + local argscount + argscount = 0 + + forward + argscount = argscount + 1 + common + if argscount and 1 + sub rsp, 8 + end if + reverse + push params + common + mov arg2, fmt + sub rsp, $20 + call __asprintf + if argscount and 1 + add rsp, $20 + 8*argscount + 8 + else + add rsp, $20 + 8*argscount + end if +} + +;aka malloc© +macro asprintf_noparams fmt* { + local fmt2 + if fmt eqtype rax + if ~(fmt in ) + mov rsi,fmt + fmt2 = rsi + else + fmt2 = fmt + end if + else + fmt2 = fmt + end if + + save_inline rsi,rdi,r12 + + or rcx, -1 + mov rdi, fmt2 + xor eax,eax + repnz scasb + neg rcx + lea r12, [rcx-1] ;r12: length + 0 terminator + + malloc r12 + if ~(fmt2 eq rsi) + mov rsi, fmt2 + end if + mov rdi, rax + mov rcx, r12 + rep movsb + + mov arg1, rax + lea rax, [r12-1] + rest +} + + +fmt equ r12 +string equ r13 + +;malloc&printf + +;stack: reverse params +;string O, fmt -> chars_len +fbound +__asprintf: + save r12,r13 + mov fmt, arg2 + lea r13, [rsp + $28 + 8 + $20] + + cinvoke vscprintf, fmt, r13 ;length (or -1 if fmt=NULL) + inc rax ;0 terminator + + malloc rax + mov arg3, r13 + mov string, rax + cinvoke vsprintf, string, fmt ;rax=len + mov arg1, string + rest + ret +restore fmt,params,string + + + +macro do_indent {ccall print_indent, indent} + +sequent equ r12 + +tside equ [sequent+SEQUENT.tside] +fside equ [sequent+SEQUENT.fside] +tlen equ [sequent+SEQUENT.tlen] +flen equ [sequent+SEQUENT.flen] +child1 equ [sequent+SEQUENT.child1] +child2 equ [sequent+SEQUENT.child2] +state equ [sequent+SEQUENT_STATE.state] + +if PRINTMODE=0 + include 'print_norm.inc' +else + include 'print_adv.inc' +end if + +restore sequent, tside,fside,tlen,flen,child1,child2 +purge do_indent + +if DEBUGSTR + include 'print_tokens.inc' +end if + +;indent +;buffer: rbx +indent equ r12 +fbound +print_indent: + test arg1,arg1 + jz .ret + + save r12 + mov indent, arg1 + align 16 + @@: + doprint s_indent, 3 + dec indent + jnz @b + rest + .ret: + ret +restore indent, buf,buflen \ No newline at end of file diff --git a/print_adv.inc b/print_adv.inc new file mode 100644 index 0000000..21f9200 --- /dev/null +++ b/print_adv.inc @@ -0,0 +1,120 @@ + +;Old, doesn't work as GUI + + +;sequent, indent +indent equ r13 + +fbound +print_seq: + save r12,r13 + mov sequent, arg1 + mov indent, arg2 + + do_indent + cinvoke printf, s_seq, sequent + + inc indent + + do_indent + cinvoke printf, s_side_t + ccall print_side, tside, tlen, indent + + do_indent + cinvoke printf, s_side_f + ccall print_side, fside, flen, indent + + do_indent + cmp child1, NULL + je .no_childs + + cinvoke puts, s_seq_childs + inc indent + + ccall print_seq, child1, indent + + cmp [sequent+SEQUENT.child2], NULL + je .one_child + ccall print_seq, child2, indent + restX + ret + + .no_childs: + movzx arg2, state + cinvoke printf, s_seq_state + .one_child: + restX + ret +restore indent + + +;side, len, indent +side equ r12 +len equ r13 +indent equ r14 + +fbound +print_side: + save r12,r13,r14,r15 + mov side, arg1 + mov len, arg2 + mov indent, arg3 + + do_indent + cinvoke printf, s_side, side + cinvoke printf, s_side_terms, len + + inc indent + xor r15,r15 + align 16 + @@: + cmp r15, len + je @f + ccall print_term, qword[side+r15*8], indent + inc r15 + jmp @b + @@: + restX + ret +restore side,len,indent + + +;term, indent +term equ r12 +indent equ r13 +fbound +print_term: + save r12,r13,r15 + mov term, arg1 + mov indent, arg2 + + do_indent + + cinvoke printf, s_term, term + movzx arg2, [term+TERM.type] + cinvoke printf, s_term_type + + inc indent + + cmp [term+TERM.type], TERM_VAR + jne @f + + ;if TERM_VAR + do_indent + lea r15, [term+TERM.t1] ;var name + cinvoke puts, r15 + jmp .ret + + @@: ;if not TERM_VAR + ccall print_term, [term+TERM.t1], indent ;print t1 + + cmp byte[term+TERM.type], TERM_NOT + jbe .ret + ;if has t2 + ccall print_term, [term+TERM.t2], indent ;print t2 + + .ret: + restX + ret + +restore term,indent \ No newline at end of file diff --git a/print_norm.inc b/print_norm.inc new file mode 100644 index 0000000..bcfc464 --- /dev/null +++ b/print_norm.inc @@ -0,0 +1,159 @@ +indent equ r13 + +;buffer, sequent, indent +fbound +print_seq: + save r12,r13,rbx,rsi,rdi + mov buf, arg1 + mov sequent, arg2 + mov indent, arg3 + + inc indent + ccall print_side, buf, tside, tlen, indent + dec indent + + do_indent + doprint s_seq_sep, 3 + + cmp child1, NULL + jne @f + cmp child2, NULL + jne @f + + cmp state, SEQUENT_CLOSED + je .closed + + doprint s_seq_open, 11 + jmp .fside + + .closed: + doprint s_seq_closed, 9 + jmp .fside + + @@: + doprint s_newline, 2 + + .fside: + inc indent + ccall print_side, buf, fside, flen, indent + + cmp child1, NULL + je @f + + do_indent + doprint s_newline, 2 + + do_indent + movzx eax, [sequent+SEQUENT_ACTION.action] + doprint [s_actions+rax*8], 8 + + ccall print_seq, buf, child1, indent + + cmp [sequent+SEQUENT.child2], NULL + je @f + + do_indent + doprint s_newline, 2 + ccall print_seq, buf, child2, indent + + @@: + rest + ret +restore indent + + +side equ r12 +len equ r13 +indent equ r14 + +;buffer, side, len, indent +fbound +print_side: + save r12,r13,r14,r15,rbx,rsi,rdi + mov buf, arg1 + mov side, arg2 + mov len, arg3 + mov indent, arg4 + + xor r15,r15 + align 16 + @@: + cmp r15, len + je @f + do_indent + ccall print_term, buf, qword[side+r15*8] + doprint s_newline, 2 + inc r15 + jmp @b + @@: + rest + ret +restore side,len,indent + + +term equ r12 + +;buffer, term +fbound +print_term: + save r12,r13,r14,rbx,rsi,rdi + mov buf, arg1 + mov term, arg2 + + mov r13b, [term+TERM.type] + test r13b,r13b + jne @f + + ;if TERM_VAR + lea rdx, [term+TERM.t1] ;var name + mov rdi, rdx + xor eax,eax + or rcx, -1 + repnz scasb + neg rcx + lea r12, [rcx-2] + mov r13, rdx ;var name + + doprint r13, r12 + resti + ret + + @@: ;if not TERM_VAR + cmp r13b, TERM_NOT + jne @f + + ;if TERM_NOT + doprint s_op_not, 1 + ccall print_term, buf, [term+TERM.t1] ;print t1 + resti + ret + + @@: ;if not TERM_NOT + doprint s_lparen, 1 + ccall print_term, buf, [term+TERM.t1] ;print t1 + + doprint s_space, 1 + movsx r13, r13b + + cmp r13, TERM_IMP + je .op_imp + ja .op_eqv + mov r14, 1 + jmp @f + .op_imp: + mov r14, 2 + jmp @f + .op_eqv: + mov r14, 3 + + @@: + doprint [s_ops+(r13-TERM_AND)*8], r14 ;print operator + doprint s_space, 1 + + ccall print_term, buf, [term+TERM.t2] ;print t2 + doprint s_rparen, 1 + + rest + ret + +restore term,indent \ No newline at end of file diff --git a/print_strings.inc b/print_strings.inc new file mode 100644 index 0000000..4e08a98 --- /dev/null +++ b/print_strings.inc @@ -0,0 +1,52 @@ +;If you change these, also change the constants after doprint uses + +s_indent db " |",0 + +s_op_not db "!",0 +s_op_and db "&",0 +s_op_or db "|",0 +s_op_imp db "->",0 +s_op_eqv db "<->",0 +s_seqsep db "@",0 + +s_lparen db "(",0 +s_rparen db ")",0 + +align 8 +s_tokens dq s_op_not +s_ops dq s_op_and, s_op_or, s_op_imp, s_op_eqv,\ + s_lparen, s_rparen, s_seqsep + +s_act_lnot db "!L ",NEWL,0 +s_act_land db "&L ",NEWL,0 +s_act_lor db "|L S ",NEWL,0 +s_act_limp db "->L S ",NEWL,0 +s_act_leqv db "<->L S",NEWL,0 +s_act_rnot db "!R ",NEWL,0 +s_act_rand db "&R S ",NEWL,0 +s_act_ror db "|R ",NEWL,0 +s_act_rimp db "->R ",NEWL,0 +s_act_reqv db "<->R S",NEWL,0 + +align 8 +s_actions dq s_act_lnot, s_act_land, s_act_lor, s_act_limp, s_act_leqv,\ + ACTION_RNOT - ACTION_LEQV - 1 dup(?),\ + s_act_rnot, s_act_rand, s_act_ror, s_act_rimp, s_act_reqv + +if PRINTMODE=0 +s_seq_sep db "--O",0 +s_seq_closed db " CLOSED",NEWL,0 +s_seq_open db " OPEN <<<",NEWL,0 + +else + +s_seq db "sequent %p",10,0 +s_seq_childs db "CHILDS:",0 +s_seq_state db "STATE: %hhu",10,0 +s_side db "side %p: ",0 +s_side_terms db "%llu term(s)",10,0 +s_side_t db "TRUE:",10,0 +s_side_f db "FALSE:",10,0 +s_term db "term %p: ",0 +s_term_type db "type %hhu",10,0 +end if \ No newline at end of file diff --git a/print_tokens.inc b/print_tokens.inc new file mode 100644 index 0000000..46f93c7 --- /dev/null +++ b/print_tokens.inc @@ -0,0 +1,36 @@ + +;Old, doesn't work as GUI + +tokens equ rsi + +;tokens +fbound +print_tokens: + save rsi + mov tokens, arg1 + + align 16 + .loop: + xor eax,eax + lodsb + test al,al + jz .done + + cmp al, TOKEN_VAR + je .var + + ;no var + cinvoke puts, [s_tokens+(rax-TOKEN_NOT)*8] + jmp .loop + + .var: + lodsq + lea arg2, [rax+1] ;skip TERM.type + ;debx arg2 + cinvoke puts, arg2 + jmp .loop + .done: + + rest + ret +restore tokens \ No newline at end of file diff --git a/proc_mod.inc b/proc_mod.inc new file mode 100644 index 0000000..6f9e094 --- /dev/null +++ b/proc_mod.inc @@ -0,0 +1,433 @@ +purge fastcall + +;Just taken from FASM source and modfified +;Now uses unaligned qwords variable +macro fastcall proc,[arg] + { common local stackspace,argscount,counter + if argscount < 4 + qwords = 4 + else + qwords = argscount + end if + counter = 0 + if qwords + if defined current@frame + if current@frame < qwords + current@frame = qwords + end if + else + if argscount and 1 + qwords = argscount+1 + end if + if qwords + sub rsp, qwords*8 + end if + end if + end if + forward + counter = counter + 1 + define type@param + define definition@param arg + match =float value,definition@param + \{ define definition@param value + define type@param float \} + match =addr value,definition@param + \{ define definition@param value + define type@param addr \} + match any=,any,definition@param + \{ \local ..string,..continue + jmp ..continue + align sizeof.TCHAR + ..string TCHAR definition@param,0 + ..continue: + define definition@param ..string + define type@param addr \} + match any,definition@param + \{ match \`any,any + \\{ \\local ..string,..continue + jmp ..continue + align sizeof.TCHAR + ..string TCHAR definition@param,0 + ..continue: + define definition@param ..string + define type@param addr \\} \} + match param,definition@param + \{ local opcode,origin + size@param = 0 + if param eqtype 0 | param eqtype 0f | type@param eq addr + size@param = 8 + else if param eqtype byte 0 | param eqtype byte 0f + match prefix value,definition@param + \\{ if prefix eq qword + size@param = 8 + else if prefix eq dword + size@param = 4 + else if prefix eq word + size@param = 2 + else if prefix eq byte + size@param = 1 + end if \\} + else if ~ param in + virtual + origin = $ + inc param + load opcode byte from origin + if opcode = 67h | opcode = 41h + load opcode byte from origin+1 + end if + if opcode and 0F8h = 48h + size@param = 8 + else if opcode = 66h + size@param = 2 + else if opcode = 0FFh + size@param = 4 + else + size@param = 1 + end if + end virtual + end if + if counter = 1 + if type@param eq float + if ~ param eq xmm0 + if size@param = 4 + if param eqtype byte 0 | param eqtype byte 0f + mov eax,param + movd xmm0,eax + else + movd xmm0,param + end if + else + if param eqtype 0 | param eqtype 0f | param eqtype byte 0 | param eqtype byte 0f + mov rax,param + movq xmm0,rax + else + movq xmm0,param + end if + end if + end if + if vararg@fastcall & ~ param eq rcx + movq rcx,xmm0 + end if + else if type@param eq addr + if ~ param eq rcx + lea rcx,[param] + end if + else if size@param = 8 + if ~ param eq rcx + mov rcx,param + end if + else if size@param = 4 + if ~ param eq ecx + mov ecx,param + end if + else if size@param = 2 + if ~ param eq cx + mov cx,param + end if + else if size@param = 1 + if ~ param eq cl + mov cl,param + end if + end if + else if counter = 2 + if type@param eq float + if ~ param eq xmm1 + if size@param = 4 + if param eqtype byte 0 | param eqtype byte 0f + mov eax,param + movd xmm1,eax + else + movd xmm1,param + end if + else + if param eqtype 0 | param eqtype 0f | param eqtype byte 0 | param eqtype byte 0f + mov rax,param + movq xmm1,rax + else + movq xmm1,param + end if + end if + end if + if vararg@fastcall & ~ param eq rdx + movq rdx,xmm1 + end if + else if type@param eq addr + if ~ param eq rdx + lea rdx,[param] + end if + else if size@param = 8 + if ~ param eq rdx + mov rdx,param + end if + else if size@param = 4 + if ~ param eq edx + mov edx,param + end if + else if size@param = 2 + if ~ param eq dx + mov dx,param + end if + else if size@param = 1 + if ~ param eq dl + mov dl,param + end if + end if + else if counter = 3 + if type@param eq float + if ~ param eq xmm2 + if size@param = 4 + if param eqtype byte 0 | param eqtype byte 0f + mov eax,param + movd xmm2,eax + else + movd xmm2,param + end if + else + if param eqtype 0 | param eqtype 0f | param eqtype byte 0 | param eqtype byte 0f + mov rax,param + movq xmm2,rax + else + movq xmm2,param + end if + end if + end if + if vararg@fastcall & ~ param eq r8 + movq r8,xmm2 + end if + else if type@param eq addr + if ~ param eq r8 + lea r8,[param] + end if + else if size@param = 8 + if ~ param eq r8 + mov r8,param + end if + else if size@param = 4 + if ~ param eq r8d + mov r8d,param + end if + else if size@param = 2 + if ~ param eq r8w + mov r8w,param + end if + else if size@param = 1 + if ~ param eq r8b + mov r8b,param + end if + end if + else if counter = 4 + if type@param eq float + if ~ param eq xmm3 + if size@param = 4 + if param eqtype byte 0 | param eqtype byte 0f + mov eax,param + movd xmm3,eax + else + movd xmm3,param + end if + else + if param eqtype 0 | param eqtype 0f | param eqtype byte 0 | param eqtype byte 0f + mov rax,param + movq xmm3,rax + else + movq xmm3,param + end if + end if + end if + if vararg@fastcall & ~ param eq r9 + movq r9,xmm3 + end if + else if type@param eq addr + if ~ param eq r9 + lea r9,[param] + end if + else if size@param = 8 + if ~ param eq r9 + mov r9,param + end if + else if size@param = 4 + if ~ param eq r9d + mov r9d,param + end if + else if size@param = 2 + if ~ param eq r9w + mov r9w,param + end if + else if size@param = 1 + if ~ param eq r9b + mov r9b,param + end if + end if + else + if type@param eq addr + lea rax,[param] + mov [rsp+(counter-1)*8],rax + else if param eqtype [0] | param eqtype byte [0] + if size@param = 8 + mov rax,param + mov [rsp+(counter-1)*8],rax + else if size@param = 4 + mov eax,param + mov [rsp+(counter-1)*8],eax + else if size@param = 2 + mov ax,param + mov [rsp+(counter-1)*8],ax + else + mov al,param + mov [rsp+(counter-1)*8],al + end if + else if size@param = 8 + virtual + origin = $ + mov rax,param + load opcode byte from origin+1 + end virtual + if opcode = 0B8h + mov rax,param + mov [rsp+(counter-1)*8],rax + else + mov qword [rsp+(counter-1)*8],param + end if + else if param in + movq [rsp+(counter-1)*8],param + else + mov [rsp+(counter-1)*8],param + end if + end if \} + common + argscount = counter + call proc + if qwords & ~defined current@frame + add rsp, qwords*8 + end if } + + + + + +purge frame +purge endf + +macro frame0 odd* { + local qwords, current + if qwords + (1-(qwords and 1)) * odd + (qwords and 1) * (1-odd) + sub rsp, (qwords + (1-(qwords and 1)) * odd + (qwords and 1) * (1-odd)) * 8 + end if + current = 0 + current@frame equ current + qwords@frame equ qwords + odd@frame equ odd +} +macro frame {frame0 FALSE} +macro frame_odd {frame0 TRUE} + +macro endfi { + local qwords + qwords = qwords@frame + (1-(qwords@frame and 1)) * odd@frame + (qwords@frame and 1) * (1-odd@frame) + if qwords + add rsp, qwords*8 + end if +} + +macro endf { + qwords@frame = current@frame + endfi + restore qwords@frame,current@frame,odd@frame +} + + +;==== For functions ==== + +macro save_func0 do_odd*, noalign*, do_save*, [arg] { + common + local argscount + argscount = 0 + forward + if do_save + argscount = argscount + 1 + if argscount <= 4 + mov [rsp + argscount*8], arg + else + push arg + end if + end if + common + local odd + odd = FALSE + + if argscount <= 4 + if do_odd + odd = TRUE + end if + else if noalign + odd = argscount and 1 + else if argscount and 1 xor do_odd + odd = TRUE + end if + + frame0 odd + + macro fin@save \{ + common + local revcount + revcount = argscount + endfi + + reverse + if do_save + if revcount > 4 + pop arg + else + mov arg, [rsp + revcount*8] + end if + revcount = revcount - 1 + end if + common + \} +} + +macro save [arg] {common save_func0 TRUE, FALSE, TRUE, arg} +macro save_nothing [arg] {common save_func0 TRUE, FALSE, FALSE} +macro save_noalign [arg] {common save_func0 NULL, TRUE, TRUE, arg} + + +;=== For inline use === + +macro save_inline0 do_odd*, noalign*, [arg] { + common + local argscount + argscount = 0 + forward + argscount = argscount + 1 + push arg + common + + frame0 noalign*(argscount and 1) + (1-noalign)*(argscount and 1 xor do_odd) + + macro fin@save \{ + common + local revcount + revcount = argscount + endfi + + reverse + pop arg + common + \} +} + +macro save_inline [arg] {common save_inline0 FALSE, FALSE, arg} +macro save_inline_odd [arg] {common save_inline0 TRUE, FALSE, arg} +macro save_inline_noalign [arg] {common save_inline0 NULL, TRUE, arg} +;save_nothing_inline would be just to use frame + + + + +macro resti {fin@save} +macro rest { + qwords@frame = current@frame + fin@save + restore qwords@frame,current@frame,odd@frame + purge fin@save +} \ No newline at end of file diff --git a/screenshots/closed.png b/screenshots/closed.png new file mode 100644 index 0000000..e7cb5ab Binary files /dev/null and b/screenshots/closed.png differ diff --git a/screenshots/open-tableau.png b/screenshots/open-tableau.png new file mode 100644 index 0000000..1f954fe Binary files /dev/null and b/screenshots/open-tableau.png differ diff --git a/screenshots/open-valuations.png b/screenshots/open-valuations.png new file mode 100644 index 0000000..775815e Binary files /dev/null and b/screenshots/open-valuations.png differ diff --git a/sequent.inc b/sequent.inc new file mode 100644 index 0000000..0d58ccb --- /dev/null +++ b/sequent.inc @@ -0,0 +1,332 @@ +SEQUENT_CLOSED = 0 +SEQUENT_OPEN = 1 + +ACTION_LNOT = 0 +ACTION_LAND = 1 +ACTION_LOR = 2 +ACTION_LIMP = 3 +ACTION_LEQV = 4 +ACTION_RNOT = 1000b+0 +ACTION_RAND = 1000b+1 +ACTION_ROR = 1000b+2 +ACTION_RIMP = 1000b+3 +ACTION_REQV = 1000b+4 + +struct SEQUENT + tside rq 1 + fside rq 1 + tlen rq 1 + flen rq 1 + child1 rq 1 + child2 rq 1 + extra rb 1 +ends + +struct SEQUENT_ACTION + tside rq 1 + fside rq 1 + tlen rq 1 + flen rq 1 + child1 rq 1 + child2 rq 1 + action rb 1 ;ACTION_* +ends + +struct SEQUENT_STATE + tside rq 1 + fside rq 1 + tlen rq 1 + flen rq 1 + child1 dq NULL + child2 dq NULL + state rb 1 ;SEQUENT_[OPEN/CLOSED] +ends + + +sequent equ r12 +tside equ [sequent+SEQUENT.tside] +fside equ [sequent+SEQUENT.fside] +tlen equ [sequent+SEQUENT.tlen] +flen equ [sequent+SEQUENT.flen] +child1 equ [sequent+SEQUENT.child1] +child2 equ [sequent+SEQUENT.child2] +state equ [sequent+SEQUENT_STATE.state] +action equ [sequent+SEQUENT_ACTION.action] + + +;n_side: 0=tside, 1=fside +macro solve_seq_side n_side* { + local ..term_loop, ..next_side, ..loop_next + +if n_side=0 + mov len, tlen +else + mov len, flen +end if + test len,len + jz ..next_side + +if n_side=0 + mov side, tside +else + mov side, fside +end if + xor el_index,el_index + ..term_loop: + mov cur_term, [side+el_index*8] ;ptr to TERM + cmp [cur_term+TERM.type], TERM_VAR + je ..loop_next + + mov last_el_index, el_index + mov last_type, [cur_term+TERM.type] + +if n_side=0 + mov jmp_table, term_t_actions_jmp + + cmp last_type, TERM_OR + jae ..loop_next +else + mov jmp_table, term_f_actions_jmp + + cmp last_type, TERM_AND + je ..loop_next + cmp last_type, TERM_EQV + je ..loop_next +end if + + jmp seq_solve.term_found + + ..loop_next: + inc el_index + cmp el_index, len + jb ..term_loop + + ..next_side: +} + + + +;childptr equ r13 +side equ r10 +len equ rcx +el_index equ r11 +jmp_table equ rax +last_type equ r9b +last_el_index equ arg2 +cur_term equ r8 + +;Solve sequent (make tree) and return if the tableau beneath is open or closed + +;TODO mode +;sequent -> SEQUENT_[OPEN/CLOSED] +fbound +seq_solve: + save r12,r13 + mov sequent, arg1 + ;mov childptr, arg2 + + ccall seq_is_closed, sequent + test rax,rax + jz .not_closed + + ;realloc sequent, sizeof.SEQUENT_STATE + ;mov sequent, rax + ;mov arg1, sequent + ;test childptr,childptr + ;jz @f + ;mov [childptr], sequent + ;@@: +if ~CHILDNULL + mov child1, NULL + mov child2, NULL +end if + + mov rax, SEQUENT_CLOSED + mov state, SEQUENT_CLOSED + resti + ret + + .not_closed: + xor last_type,last_type + + + solve_seq_side 1 ;fside has less splitting actions + solve_seq_side 0 + + + test last_type,last_type + jz .open_leaf + + ;if no nonsplitting found, take last splitting + .term_found: + cmp jmp_table, term_f_actions_jmp + sete r8b + shl r8b, 3 + or r8b, last_type + dec r8b ;-TERM_NOT + mov action, r8b + + movzx r9d, last_type + ccall qword[jmp_table+(r9-TERM_NOT)*8], sequent ;, el_index + + ;lea arg2, [sequent+SEQUENT.child1] + ccall seq_solve, child1 + + cmp child2, NULL + je .one_child + + mov r13, rax + ;lea arg2, [sequent+SEQUENT.child2] + ccall seq_solve, child2 + test r13,r13 + jnz .open + test rax,rax + jnz .open + + ;mov arg1, sequent + mov rax, SEQUENT_CLOSED + resti + ret + + .open_leaf: + ;realloc sequent, sizeof.SEQUENT_STATE + ;mov sequent, rax + mov state, SEQUENT_OPEN + ;mov arg1, sequent + ;test childptr,childptr + ;jz .open + ;mov [childptr], sequent + +if ~CHILDNULL + mov child1, NULL + mov child2, NULL +end if + + .open: + mov rax, SEQUENT_OPEN + + .one_child: ;return result of ccall solve_seq, child1 + ;mov arg1, sequent + rest + ret + +restore side,len,el_index,jmp_table,last_term,last_type,cur_term,last_el_index ;,childptr +purge solve_seq_side + + +;TODO check contents? + +;Is sequent closed? (same terms on both sides) +;closed=0/1 +;Only checks addresses, not contents (hence tokens_group_vars is necessary) + +;sequent -> closed +fbound +seq_is_closed: + save rsi,rdi + mov sequent, arg1 + + cmp tlen, 0 + jz .not_closed + cmp flen, 0 + jz .not_closed + + mov rsi, tside + mov rdx, tlen + + mov r8, fside + mov r9, flen + @@: + lodsq + mov rdi, r8 ;fside + mov rcx, r9 ;flen + repne scasq + je .closed + dec rdx + jnz @b + + .not_closed: + xor eax,eax + resti + ret + + .closed: + mov rax, TRUE + rest + ret + + +if FALSE ;seq_is_open is not really needed anymore + +;Is sequent open? (only TERMVARS and not closed) + +;sequent -> open +fbound +seq_is_open: + save rsi,rdi + mov sequent, arg1 + + macro check_side@seq_is_open side*, len* { + mov rsi, side + mov rdx, len + + @@: + lodsq + cmp [rax+TERM.type], TERM_VAR + jne .not_open + dec rdx + jnz @b + } + + cmp [rcx+SEQUENT.tlen], 0 + jz .check_fside + check_side@seq_is_open [rcx+SEQUENT.tside], [rcx+SEQUENT.tlen] + + .check_fside: + cmp [rcx+SEQUENT.flen], 0 + jz .open + check_side@seq_is_open [rcx+SEQUENT.fside], [rcx+SEQUENT.flen] + + purge check_side@seq_is_open + + .open: + mov rax, TRUE + resti + ret + + .not_open: + xor eax,eax + rest + ret +end if + + +;TODO use stack instead of recursion + +;Free sequent and child sequents (etc) and sides of sequents +;Does not free terms + +;sequent +fbound +seq_free: + save r12 + mov sequent, arg1 + + mfree tside + mfree fside + + cmp child1, NULL + je @f + ccall seq_free, child1 + + cmp child2, NULL + je @f + ccall seq_free, child2 + + @@: + mfree sequent + + rest + ret + +restore sequent, tside,fside,tlen,flen,child1,child2 \ No newline at end of file diff --git a/term.inc b/term.inc new file mode 100644 index 0000000..775589f --- /dev/null +++ b/term.inc @@ -0,0 +1,77 @@ +TERM_VAR = 0 +TERM_NOT = 1 +TERM_AND = 2 +TERM_OR = 3 +TERM_IMP = 4 +TERM_EQV = 5 + +;I will often refer to TERMVAR & TERM1 structs as just TERM +struct TERMVAR + type db TERM_VAR + t1 rb 0 ;string of some length, NULL-terminated +ends + +struct TERM1 + type rb 1 ;one of TERM_* + t1 rq 1 ;ptr to TERM +ends + +struct TERM TERM1 + t2 rq 1 ;ptr to TERM +ends + + +term equ r12 + +;Free term and child terms +;Does not free TERMVARs + +;term +fbound +term_free: + push NULL + push arg1 + + .loop: + pop rax + test rax,rax ;is NULL? + jz .done + + mov cl, [rax+TERM.type] + test cl,cl + jz .loop ;skip vars + + push [rax+TERM.t1] + + cmp cl, TERM_AND + jb @f + + push [rax+TERM.t2] + + bt rsp, 3 + jc .align_free + + frame + mfree rax + endf + jmp .loop + + @@: ;TERM1 + bt rsp, 3 + jc .align_free + + frame + mfree rax + endf + jmp .loop + + .align_free: + ;align stack + frame_odd + mfree rax + endf + jmp .loop + + .done: + ret +restore term \ No newline at end of file diff --git a/term_actions.inc b/term_actions.inc new file mode 100644 index 0000000..f16b3d9 --- /dev/null +++ b/term_actions.inc @@ -0,0 +1,530 @@ +CHILDNULL = FALSE + +macro action_not sidefrom*, sideto*, lenfrom*, lento* { + save r12,r13,r14,r15,rsi,rdi + mov sequent, arg1 + mov el_index, arg2 + + malloc sizeof.SEQUENT + mov new_seq, rax + mov child1, new_seq + mov child2, NULL + +if CHILDNULL + mov [new_seq+SEQUENT.child1], NULL + mov [new_seq+SEQUENT.child2], NULL +end if + + ;===sideto=== + mov r15, lento + inc r15 ;r15 = incremented lento + shl r15, 3 ;*8 + + malloc r15 ;alloc 8*(lento+1) + + ;copy old to new + mov rsi, sideto ;rsi = old sideto + mov rdi, rax ;rdi = new sideto + mov rcx, lento ;rcx = lento + rep movsq + + + ;add elem sidefrom[el_index].t1 + mov r11, sidefrom ;sidefrom ptr + mov r11, [r11+el_index*8] ;elem ptr + mov r11, [r11+TERM.t1] ;elem.t1 (=TERM ptr) + sub r15, 8 + mov [rax+r15], r11 ;new sideto[(old)lento*8] = elem.t1 + + ;update sideto + mov [new_seq+SEQUENT.#sideto], rax + ;update lento + mov r11, lento + inc r11 + mov [new_seq+SEQUENT.#lento], r11 + + + ;===sidefrom=== + dec_lenfrom equ r15 + mov dec_lenfrom, lenfrom + dec dec_lenfrom + mov r11, dec_lenfrom + shl r11, 3 + malloc r11 ;alloc 8*(lenfrom-1) + + mov rsi, sidefrom ;rsi = old sidefrom + mov rdi, rax ;rdi = new sidefrom + mov rcx, el_index ;rcx = el_index + rep movsq + + add rsi, 8 ;skip elem + mov rcx, dec_lenfrom ;rcx = lenfrom-1 + sub rcx, el_index ;rcx = lenfrom-1 - elem_index + rep movsq + + + ;update sidefrom + mov [new_seq+SEQUENT.#sidefrom], rax + ;update lenfrom + mov r11, lenfrom + dec r11 + mov [new_seq+SEQUENT.#lenfrom], r11 + + rest + ret +} + + +macro action_chop side1*, side2*, len1*, len2* { + save r12,r13,r14,r15,rsi,rdi + mov sequent, arg1 + mov el_index, arg2 + + malloc sizeof.SEQUENT + mov new_seq, rax + mov child1, new_seq + mov child2, NULL + +if CHILDNULL + mov [new_seq+SEQUENT.child1], NULL + mov [new_seq+SEQUENT.child2], NULL +end if + + ;===side1=== + inc_len1 equ r15 + mov inc_len1, len1 + inc inc_len1 + mov r11, inc_len1 + shl r11, 3 + malloc r11 ;alloc 8*(len1 + 1) + + mov rsi, side1 ;rsi = old side1 + mov rdi, rax ;rdi = new side1 + mov rcx, el_index ;rcx = el_index + rep movsq + + add rsi, 8 ;skip elem + mov rcx, len1 + dec rcx ;rcx = len1 - 1 + sub rcx, el_index ;rcx = len1 - 1 - elem_index + rep movsq + + ;add elems + mov rsi, side1 ;side1 ptr + mov rsi, [rsi+el_index*8] ;elem ptr + add rsi, TERM.t1 ;elem.t1 (=TERM ptr) + movsq ;add to new side1: elem.t1 + movsq ;add to new side1: elem.t2 + + mov [new_seq+SEQUENT.#side1], rax ;update side1 + mov [new_seq+SEQUENT.#len1], inc_len1 ;update len1 + + + ;===side2=== + mov rax, len2 + shl rax, 3 + malloc rax ;alloc 8*len2 + + mov rsi, side2 ;rsi = old side2 + mov rdi, rax ;rdi = new side2 + mov rcx, len2 ;rcx = len2 + rep movsq + + mov [new_seq+SEQUENT.#side2], rax ;update side2 + mov rax, len2 + mov [new_seq+SEQUENT.#len2], rax ;update len2 + + rest + ret +} + + +;side1 contains element to be chopped and will receive the chopped terms (excl. t1 if t1_at2) +macro action_chop_split side1*, side2*, len1*, len2*, t1_at2=FALSE { + seq1 equ r14 + seq2 equ rbx + + save r12,r13,r14,r15,rbx,rsi,rdi + mov sequent, arg1 + mov el_index, arg2 + + macro create_seq@action_chop_split n_seq* \{ + malloc sizeof.SEQUENT + + mov seq\#n_seq, rax + mov child\#n_seq, rax + +if CHILDNULL + mov [rax+SEQUENT.child1], NULL + mov [rax+SEQUENT.child2], NULL +end if + \} + + rept 2 % \{create_seq@action_chop_split %\} + purge create_seq@action_chop_split + + ;===side1=== +if ~t1_at2 + mov r15, len1 + shl r15, 3 +end if + + macro side1@action_chop_split n_child* \{ + if t1_at2 + mov r15, len1 + if n_child=1 + dec r15 + end if + shl r15, 3 + end if + malloc r15 ;alloc 8*(len1 [-1]) + + mov rsi, side1 ;rsi = old side1 + mov rdi, rax ;rdi = new side1 + mov rcx, el_index ;rcx = el_index + rep movsq + + add rsi, 8 ;skip elem + mov rcx, len1 + dec rcx ;rcx = len1 - 1 + sub rcx, el_index ;rcx = len1 - 1 - elem_index + rep movsq + + if ~(t1_at2 & n_child=1) + ;add elem.tX + mov rsi, side1 ;side1 ptr + mov rsi, [rsi+el_index*8] ;elem ptr + add rsi, TERM.t\#n_child ;elem.tX (=TERM ptr) + movsq ;add to new side1: elem.tX + end if + + mov [seq\#n_child+SEQUENT.#side1], rax ;update side1 + mov rax, len1 + if t1_at2 & n_child=1 + dec rax + end if + mov [seq\#n_child+SEQUENT.#len1], rax ;set len1 + \} + + rept 2 % \{side1@action_chop_split %\} + purge side1@action_chop_split + + ;===side2=== +if ~t1_at2 + mov r15, len2 + shl r15, 3 +end if + + macro side2@action_chop_split n_child* \{ + if t1_at2 + mov r15, len2 + if n_child=1 + inc r15 + end if + shl r15, 3 + end if + malloc r15 ;alloc 8*(len2 [+1]) + + mov rsi, side2 ;rsi = old side2 + mov rdi, rax ;rdi = new side2 + mov rcx, len2 ;rcx = len2 + rep movsq + + if t1_at2 & n_child=1 + ;add elem.t1 + mov rsi, side1 ;side1 ptr + mov rsi, [rsi+el_index*8] ;elem ptr + add rsi, TERM.t1 ;elem.t1 (=TERM ptr) + movsq ;add to new side2: elem.t1 + end if + + mov [seq\#n_child+SEQUENT.#side2], rax ;update side2 + mov rax, len2 + if t1_at2 & n_child=1 + inc rax + end if + mov [seq\#n_child+SEQUENT.#len2], rax ;set len2 + \} + + rept 2 % \{side2@action_chop_split %\} + purge side2@action_chop_split + + rest + ret + restore seq1,seq2 +} + + +;side1 contains element to be chopped +macro action_imp_eqv_r side1*, side2*, len1*, len2*, split* { + seq1 equ r14 + seq2 equ rbx + + save r12,r13,r14,r15,rbx,rsi,rdi + mov sequent, arg1 + mov el_index, arg2 + + macro create_seq@action_imp_eqv_r n_seq* \{ + malloc sizeof.SEQUENT + + mov seq\#n_seq, rax + mov child\#n_seq, rax + +if CHILDNULL + mov [rax+SEQUENT.child1], NULL + mov [rax+SEQUENT.child2], NULL +end if + \} + + create_seq@action_imp_eqv_r 1 +if split + create_seq@action_imp_eqv_r 2 +else + mov child2, NULL +end if + purge create_seq@action_imp_eqv_r + + ;===side1=== + mov r15, len1 + shl r15, 3 + + macro side1@action_imp_eqv_r n_child*, tx* \{ + malloc r15 ;alloc 8*len1 + + mov rsi, side1 ;rsi = old side1 + mov rdi, rax ;rdi = new side1 + mov rcx, el_index ;rcx = el_index + rep movsq + + add rsi, 8 ;skip elem + mov rcx, len1 + dec rcx ;rcx = len1 - 1 + sub rcx, el_index ;rcx = len1 - 1 - elem_index + rep movsq + + ;add elem.tX + mov rsi, side1 ;side1 ptr + mov rsi, [rsi+el_index*8] ;elem ptr + add rsi, TERM.t\#tx ;elem.tX (=TERM ptr) + movsq ;add to new side1: elem.tX + + mov [seq\#n_child+SEQUENT.#side1], rax ;update side1 + mov rax, len1 + mov [seq\#n_child+SEQUENT.#len1], rax ;set len1 + \} + + ;child1 gets t2, child2 gets t1 + side1@action_imp_eqv_r 1, 2 +if split + side1@action_imp_eqv_r 2, 1 +end if + purge side1@action_imp_eqv_r + + ;===side2=== + mov r15, len2 + inc r15 + shl r15, 3 + + macro side2@action_imp_eqv_r n_child* \{ + malloc r15 ;alloc 8*(len2 + 1) + + mov rsi, side2 ;rsi = old side2 + mov rdi, rax ;rdi = new side2 + mov rcx, len2 ;rcx = len2 + rep movsq + + ;add elem.tX + mov rsi, side1 ;side1 ptr + mov rsi, [rsi+el_index*8] ;elem ptr + add rsi, TERM.t\#n_child ;elem.tX (=TERM ptr) + movsq ;add to new side2: elem.tX + + mov [seq\#n_child+SEQUENT.#side2], rax ;update side2 + mov rax, len2 + inc rax + mov [seq\#n_child+SEQUENT.#len2], rax ;set len2 + \} + + side2@action_imp_eqv_r 1 +if split + side2@action_imp_eqv_r 2 +end if + purge side2@action_imp_eqv_r + + rest + ret + restore seq1,seq2 +} + + +;side1 contains element to be chopped +macro action_eqv_l side1*, side2*, len1*, len2* { + seq1 equ r14 + seq2 equ rbx + + save r12,r13,r14,r15,rbx,rsi,rdi + mov sequent, arg1 + mov el_index, arg2 + + macro create_seq@action_eqv_l n_seq* \{ + malloc sizeof.SEQUENT + + mov seq\#n_seq, rax + mov child\#n_seq, rax + +if CHILDNULL + mov [rax+SEQUENT.child1], NULL + mov [rax+SEQUENT.child2], NULL +end if + \} + + rept 2 % \{create_seq@action_eqv_l %\} + purge create_seq@action_eqv_l + + ;===side1=== + mov r15, len1 + inc r15 + shl r15, 3 + + macro side1@action_eqv_l n_child* \{ + if n_child=2 + sub r15, 2*8 + end if + malloc r15 ;alloc 8*(len1 + 1) + + mov rsi, side1 ;rsi = old side1 + mov rdi, rax ;rdi = new side1 + mov rcx, el_index ;rcx = el_index + rep movsq + + add rsi, 8 ;skip elem + mov rcx, len1 + dec rcx ;rcx = len1 - 1 + sub rcx, el_index ;rcx = len1 - 1 - elem_index + rep movsq + + if n_child=1 + ;add elems + mov rsi, side1 ;side1 ptr + mov rsi, [rsi+el_index*8] ;elem ptr + add rsi, TERM.t1 ;elem.t1 (=TERM ptr) + movsq ;add to new side1: elem.t1 + movsq ;add to new side1: elem.t2 + end if + + mov [seq\#n_child+SEQUENT.#side1], rax ;update side1 + mov rax, len1 + if n_child=1 + inc rax + else + dec rax + end if + mov [seq\#n_child+SEQUENT.#len1], rax ;set len1 + \} + + rept 2 % \{side1@action_eqv_l %\} + purge side1@action_eqv_l + + ;===side2=== + mov r15, len2 + shl r15, 3 + + macro side2@action_eqv_l n_child* \{ + if n_child=2 + add r15, 2*8 + end if + malloc r15 ;alloc 8*len2 + + mov rsi, side2 ;rsi = old side2 + mov rdi, rax ;rdi = new side2 + mov rcx, len2 ;rcx = len2 + rep movsq + + if n_child=2 + ;add elems + mov rsi, side1 ;side1 ptr + mov rsi, [rsi+el_index*8] ;elem ptr + add rsi, TERM.t1 ;elem.t1 (=TERM ptr) + movsq ;add to new side2: elem.t1 + movsq ;add to new side2: elem.t2 + end if + + mov [seq\#n_child+SEQUENT.#side2], rax ;update side2 + mov rax, len2 + if n_child=2 + add rax, 2 + end if + mov [seq\#n_child+SEQUENT.#len2], rax ;set len2 + \} + + rept 2 % {side2@action_eqv_l %\} + purge side2@action_eqv_l + + rest + ret + restore seq1,seq2 +} + + + +sequent equ r12 +el_index equ r13 +new_seq equ r14 + +tside equ [sequent+SEQUENT.tside] +fside equ [sequent+SEQUENT.fside] +tlen equ [sequent+SEQUENT.tlen] +flen equ [sequent+SEQUENT.flen] +child1 equ [sequent+SEQUENT.child1] +child2 equ [sequent+SEQUENT.child2] + + +t_actions: + +;sequent, el_index +fbound +.not: action_not tside, fside, tlen, flen + +;sequent, el_index +fbound +.and: action_chop tside, fside, tlen, flen + +;sequent, el_index +fbound +.or: action_chop_split tside, fside, tlen, flen + +;sequent, el_index +fbound +.imp: action_chop_split tside, fside, tlen, flen, TRUE + +;sequent, el_index +fbound +.eqv: action_eqv_l tside, fside, tlen, flen + + +f_actions: + +;sequent, el_index +fbound +.not: action_not fside, tside, flen, tlen + +;sequent, el_index +fbound +.and: action_chop_split fside, tside, flen, tlen + +;sequent, el_index +fbound +.or: action_chop fside, tside, flen, tlen + +;sequent, el_index +fbound +.imp: action_imp_eqv_r fside, tside, flen, tlen, FALSE + +;sequent, el_index +fbound +.eqv: action_imp_eqv_r fside, tside, flen, tlen, TRUE + + + +restore sequent,el_index, new_seq, tside,fside,tlen,flen,child1,child2 +purge action_not,action_chop,action_chop_split,action_imp_eqv_r diff --git a/tokens.inc b/tokens.inc new file mode 100644 index 0000000..19c83f9 --- /dev/null +++ b/tokens.inc @@ -0,0 +1,516 @@ +TOKEN_END = 0 +TOKEN_VAR = 1 +TOKEN_NOT = 2 +TOKEN_AND = 3 +TOKEN_OR = 4 +TOKEN_IMP = 5 +TOKEN_EQV = 6 +TOKEN_LPAREN = 7 +TOKEN_RPAREN = 8 +TOKEN_SEQSEP = 9 + + +struct TOKEN + type rb 1 ;TOKEN_* +ends +struct TOKENVAROFF + type db TOKEN_VAR + offset rd 1 ;offset in string + pad rd 1 +ends +struct TOKENVAR + type db TOKEN_VAR + term rq 1 ;ptr to TERMVAR +ends + +string equ r12 +tokens equ r13 +tokens_lenb equ r14 +tokens_len equ rbx +var_offset equ edi +var_offsetm equ rdi ;(mask) bit 63 is set if we are not reading a var + +;TODO more operator aliases ('=', '==') +;TODO remove tokens_len? + +;Tokenizes string and +; on success, error=0 and tokens is a malloced TOKEN/TOKENVAR array and tokens_len the length number of tokens +; on error, error is a malloced error string + +;string, tokens O, tokens_len O -> error +fbound +tokenize: + save r12,r13,r14,r15,rbx,rsi,rdi + mov string, arg1 + + xor tokens_lenb,tokens_lenb + xor tokens_len,tokens_len + bts var_offsetm, 63 + + malloc tokens_lenb + mov tokens, rax + + mov rsi, string + align 16 + .loop: + lodsb + test al,al + jz .done + + cmp al, 'A' + jb .no_letter + cmp al, 'z' + ja .no_letter + cmp al, 'Z' + jbe .letter + cmp al, 'a' + jb .no_letter + + .letter: ;I could use a loop here, but.. this works + bt var_offsetm, 63 + jnc .loop + lea var_offsetm, [rsi-1] + sub var_offsetm, string + jmp .loop + + .no_letter: + bts var_offsetm, 63 + jc .no_append_var + + ;append var + add tokens_lenb, sizeof.TOKENVAR + inc tokens_len + mov r15b, al + realloc tokens, tokens_lenb + mov tokens, rax + mov al, r15b + + mov [tokens+tokens_lenb-sizeof.TOKENVAR+TOKEN.type], TOKEN_VAR + mov [tokens+tokens_lenb-sizeof.TOKENVAR+TOKENVAROFF.offset], var_offset + bts var_offsetm, 63 + mov byte[rsi-1], 0 ;write 0 terminator + + .no_append_var: + + cmp al, ' ' + je .loop + + cmp al, '(' + je .token_lparen + + cmp al, ')' + je .token_rparen + + cmp al, '!' + je .token_not + + cmp al, '&' + je .token_and + + cmp al, '|' + je .token_or + + cmp al, '-' + je .token_dash + + cmp al, '<' + je .token_lt + + cmp al, '/' + je .token_slash + + cmp al, '\' + je .token_backslash + + cmp al, '~' + je .token_not + + cmp al, 9 ;tab + je .loop + cmp al, 10 ;LF + je .loop + cmp al, 13 ;CR + je .loop + + cmp al, '@' + je .token_sep + + jmp .error_unknown + + .append: + inc tokens_lenb + inc tokens_len + mov r15b, al + realloc tokens, tokens_lenb + mov tokens, rax + mov al, r15b + + mov [tokens+tokens_lenb-1+TOKEN.type], al + jmp .loop + + .error_unexpected_gt: + test al,al + jz @f + movzx eax, al + jmp .error_unexpected_gt.print + @@: + mov rax, 'E' + .error_unexpected_gt.print: + sub rsi, string + asprintf s_tok_e_unexpected, ('>'), rax, rsi + jmp .error + + .error_unexpected_dash: + test al,al + jz @f + movzx eax, al + jmp .error_unexpected_dash.print + @@: + mov rax, 'E' + .error_unexpected_dash.print: + sub rsi, string + asprintf s_tok_e_unexpected, ('-'), rax, rsi + jmp .error + + .error_unexpected_backslash: + test al,al + jz @f + movzx eax, al + jmp .error_unexpected_backslash.print + @@: + mov rax, 'E' + .error_unexpected_backslash.print: + sub rsi, string + asprintf s_tok_e_unexpected, ('\'), rax, rsi + jmp .error + + .error_unexpected_slash: + test al,al + jz @f + movzx eax, al + jmp .error_unexpected_slash.print + @@: + mov rax, 'E' + .error_unexpected_slash.print: + sub rsi, string + asprintf s_tok_e_unexpected, ('/'), rax, rsi + jmp .error + + .error_unknown: + movzx eax, al + sub rsi, string + asprintf s_tok_e_unknown, rax, rsi + + .error: + mov r12, arg1 + mfree tokens + mov rax, r12 + resti + ret + + .done: + bt var_offsetm, 63 + jc @f + + ;append var + add tokens_lenb, sizeof.TOKENVAR + inc tokens_len + realloc tokens, tokens_lenb + mov tokens, rax + + mov [tokens+tokens_lenb-sizeof.TOKENVAR+TOKEN.type], TOKEN_VAR + mov [tokens+tokens_lenb-sizeof.TOKENVAR+TOKENVAROFF.offset], var_offset + + @@: + ;append end token + inc tokens_lenb + inc tokens_len + realloc tokens, tokens_lenb + mov tokens, rax + mov [tokens+tokens_lenb-1+TOKEN.type], TOKEN_END + + xor eax,eax + mov arg2, tokens + mov arg3, tokens_len + rest + ret + + +fbound +.token_lparen: + mov al, TOKEN_LPAREN + jmp .append + +fbound +.token_rparen: + mov al, TOKEN_RPAREN + jmp .append + +fbound +.token_not: + mov al, TOKEN_NOT + jmp .append + +fbound +.token_and: + cmp byte[rsi], '&' + je .token_and.inc + mov al, TOKEN_AND + jmp .append + + .token_and.inc: + inc rsi + mov al, TOKEN_AND + jmp .append + +fbound +.token_or: + cmp byte[rsi], '|' + je .token_or.inc + mov al, TOKEN_OR + jmp .append + + .token_or.inc: + inc rsi + mov al, TOKEN_OR + jmp .append + +fbound +.token_sep: + mov al, TOKEN_SEQSEP + jmp .append + +fbound +.token_dash: + lodsb + cmp al, '>' + jne .error_unexpected_gt + mov al, TOKEN_IMP + jmp .append + +fbound +.token_lt: + lodsb + cmp al, '-' + jne .error_unexpected_dash + lodsb + cmp al, '>' + jne .error_unexpected_gt + mov al, TOKEN_EQV + jmp .append + +fbound +.token_slash: + lodsb + cmp al, '\' + jne .error_unexpected_backslash + mov al, TOKEN_AND + jmp .append + +fbound +.token_backslash: + lodsb + cmp al, '/' + jne .error_unexpected_slash + mov al, TOKEN_OR + jmp .append + +restore string,tokens,tokens_len,tokens_lenb,var_offset,var_offsetm + + + +string equ r12 +tokens equ rsi +vars equ r13 +vars_lenb equ r14 +cur_name equ r15 + +;Group variables of sequent and transform TOKENVAROFFs to TOKENVARs +;Data pointed to by tokens will be updated, vars will contain TERMVARs and vars_len is the number of TERMVARs + +;string, tokens, vars O, vars_len O +fbound +tokens_group_vars: + save r12,r13,r14,r15,rbx,rsi,rdi + mov string, arg1 + mov tokens, arg2 + + xor vars_lenb,vars_lenb + malloc vars_lenb + mov vars, rax + + align 16 + .loop: + lodsb + test al,al + jz .done + + cmp al, TOKEN_VAR + jne .loop + + xor eax,eax + lodsd + lea cur_name, [string+rax] + lodsd ;skip pad + + xor ecx,ecx ;byte index in vars + + mov rbx, tokens ;save + align 16 + .equalvarloop: + cmp rcx, vars_lenb + je .no_vars_equal + + mov rsi, cur_name + mov rdi, [vars+rcx] + inc rdi ;skip TERM.type + + .equalcharloop: + cmpsb + jne .var_not_equal + cmp byte[rsi-1], 0 + jnz .equalcharloop + jmp .var_equal ;end reached + + .var_not_equal: + add rcx, 8 + jmp .equalvarloop + + .no_vars_equal: ;add var + add vars_lenb, 8 + realloc vars, vars_lenb + mov vars, rax + + ;find length + mov rdi, cur_name + or rcx, -1 + xor al,al + repne scasb ;search for 0 terminator + neg rcx ;rcx: length + 0 terminator + type + + mov rdi, rcx ;save termsize + malloc rcx ;allocate TERMVAR including type + mov rcx, rdi ;restore termsize for rep movsb + mov [vars+vars_lenb-8], rax ;add ptr to new TERMVAR to vars + + ;init new TERMVAR + mov [rax+TERM.type], TERM_VAR ;set type + ;set name + mov rsi, cur_name + lea rdi, [rax+TERM.t1] + dec rcx ;-TERM.t1 + rep movsb ;also uses rcx + + mov tokens, rbx ;restore + mov [tokens-sizeof.TOKENVAR.term], rax ;change offset to ptr to new TERMVAR in tokens + jmp .loop + + .var_equal: ;[vars+rcx] = ptr to TERMVAR + mov tokens, rbx ;restore + + mov rcx, [vars+rcx] + mov [tokens-sizeof.TOKENVAR.term], rcx ;change offset to ptr to existing TERMVAR in tokens + jmp .loop + + .done: + mov arg3, vars + mov arg4, vars_lenb + shr arg4, 3 + rest + ret +restore string,tokens,vars,vars_lenb,cur_name + + + +split_sides.ERR_NO_SEP = 1 +split_sides.ERR_MULTIPLE_SEPS = 2 + +fside equ arg2 + +;Split sides of tokens on the TOKEN_SEP +; on success, fside will be a pointer to the fside, which is now preceded by a TOKEN_END instead of a TOKEN_SEP and error=0 +; on error, error is one of split_sides.ERR_* + +;tokens, fside O -> error +fbound +split_sides: + save rsi + mov rsi, arg1 + + align 16 + .loop: + lodsb + cmp al, TOKEN_SEQSEP + je .found + + test al,al + jz .none + + cmp al, TOKEN_VAR + jne .loop + lodsq + jmp .loop + + .found: + mov fside, rsi + + align 16 + .notmoreloop: + lodsb + test al,al + jz .done + + cmp al, TOKEN_VAR + jne @f + lodsq + jmp .notmoreloop + + @@: + cmp al, TOKEN_SEQSEP + jne .notmoreloop + jmp .multiple + + .none: + mov rax, split_sides.ERR_NO_SEP + resti + ret + + .multiple: + mov rax, split_sides.ERR_MULTIPLE_SEPS + resti + ret + + .done: + mov byte[fside-1], TOKEN_END + xor eax,eax + rest + ret +restore sep_pos + + +vars_orig equ r12 +vars_len equ r13 + +;Free vars_len variables in vars + +;vars, vars_len +fbound +free_variables: + save r12,r13,rsi + mov vars_orig, arg1 + test arg2,arg2 + jz .free_vars_done + mov vars_len, arg2 + + mov rsi, arg1 + align 16 + .free_vars_loop: + lodsq + mfree rax + dec vars_len + jnz .free_vars_loop + .free_vars_done: + mfree vars_orig + rest + ret +restore vars_orig, vars_len