Skip to content

Commit

Permalink
Rewriter fixes for amd64 verification
Browse files Browse the repository at this point in the history
  • Loading branch information
@zyedidia
zyedidia committed Jun 17, 2024
1 parent 0817920 commit 2836fb4
Show file tree
Hide file tree
Showing 3 changed files with 88 additions and 30 deletions.
92 changes: 62 additions & 30 deletions lfi-leg/lfi-amd64.leg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,12 +110,13 @@ setguardrdi(Transform* t, size_t n, char** x)
} \
%}

Top = Insn* !.
# Top = Insn* !.

Insn = INDENT Label? (
FnDirective
| Directive
| Leave
| ModLeaSP
| Lea
| Stos
| Movs
Expand All @@ -129,6 +130,7 @@ Insn = INDENT Label? (
| Load
| Access
| Branch
| BranchMem
| BranchMemSafe
| CallInd
| CallIndMem
Expand Down Expand Up @@ -268,19 +270,7 @@ Addr = (
}
}
# imm(...)
| (i:IMM b:AddrRegReg) {
$$ = (Transform) {
.val = xasprintf("%%gs:(%%r15d)"),
.valrdi = xasprintf("%%gs:(%%edi)"),
.post = strdup("movq %r15, %rdi"),
};
setguard(&$$, 1, (char*[]){ xasprintf("leaq %s%s, %%r15", i.val, b.val) });
setguardrdi(&$$, 2, (char*[]){
xasprintf("movq %%rdi, %%r15"),
xasprintf("leaq %s%s, %%rdi", i.val, b.val),
});
}
| (i:IMM b:AddrRegRegImm) {
| (i:IMM b:AddrRegDisp) {
$$ = (Transform) {
.val = xasprintf("%%gs:(%%r15d)"),
.valrdi = xasprintf("%%gs:(%%edi)"),
Expand All @@ -293,7 +283,7 @@ Addr = (
});
}
# (...)
| (b:AddrRegReg) {
| (b:AddrRegDisp) {
$$ = (Transform) {
.val = xasprintf("%%gs:(%%r15d)"),
.valrdi = xasprintf("%%gs:(%%edi)"),
Expand All @@ -305,26 +295,26 @@ Addr = (
xasprintf("leaq %s, %%rdi", b.val),
});
}
| (b:AddrRegRegImm) {
# imm
| (n:NUM &(- (EOL | ';' | ','))) {
$$ = (Transform) {
.val = xasprintf("%%gs:(%%r15d)"),
.valrdi = xasprintf("%%gs:(%%edi)"),
.post = strdup("movq %r15, %rdi"),
.val = xasprintf("%%gs:%s", n.val)
};
setguard(&$$, 1, (char*[]){ xasprintf("leaq %s, %%r15", b.val) });
setguardrdi(&$$, 2, (char*[]){
xasprintf("movq %%rdi, %%r15"),
xasprintf("leaq %s, %%rdi", b.val),
});
tfree(n);
}
)

AddrRegReg = '(' (!AddrReg r1:REG) COMMA (!AddrReg r2:REG) ')' {
AddrRegDisp = AddrRegReg | AddrRegRegImm | AddrRegImm

AddrRegReg = LP (!AddrReg r1:REG) COMMA (!AddrReg r2:REG) RP {
$$ = (Transform) { .val = xasprintf("(%s, %s)", r1.val, r2.val) }
}
AddrRegRegImm = '(' (!AddrReg r1:REG) COMMA (!AddrReg r2:REG) (COMMA i:IMM) ')' {
AddrRegRegImm = LP (!AddrReg r1:REG) COMMA (!AddrReg r2:REG) COMMA i:IMM RP {
$$ = (Transform) { .val = xasprintf("(%s, %s, %s)", r1.val, r2.val, i.val) }
}
AddrRegImm = LP COMMA (!AddrReg r2:REG) COMMA i:IMM RP {
$$ = (Transform) { .val = xasprintf("(, %s, %s)", r2.val, i.val) }
}

AddrReg = 'rsp' | 'rip'

Expand Down Expand Up @@ -391,6 +381,16 @@ Call = 'call' 'q'? - rest:ITEM {
tfree(rest);
}

BranchMem = j:JMP - '*' a:Addr {
mkguards(a);
mkinsn("movq %s, %%r15\n", a.val);
mkcodedirective(".p2align 4\n");
mkinsn("andl $0xfffffff0, %%r15d\n");
mkinsn("orq %%r14, %%r15\n");
mkinsn("%s *%%r15\n", j.val);
tfree(j); tfree(a);
}

BranchMemSafe = j:JMP - '*' a:AddrNoMod {
mkinsn("movq %s, %%r15\n", a.val);
mkcodedirective(".p2align 4\n");
Expand All @@ -409,8 +409,10 @@ Branch = j:JMP '*' r:XREG {
}

Leave = 'leave' 'q'? - {
mkcodedirective(".bundle_lock\n");
mkinsn("movl %%ebp, %%esp\n");
mkinsn("orq %%r14, %%rsp\n");
mkcodedirective(".bundle_unlock\n");
mkinsn("popq %%rbp\n");
}

Expand All @@ -436,17 +438,43 @@ Syscall = (( 'syscall' - ) | ( 'int' - '0x80' - )) {

ModSP = ModImmSP | ModRegSP

AddrBP = (
# imm(...)
(i:IMM_VAR LP r:XREG RP) {
$$ = (Transform) {
.val = xasprintf("%s(%s)", i.val, lo(r.val)),
}
}
# (...)
| (LP r:XREG RP) {
$$ = (Transform) {
.val = xasprintf("(%s)", lo(r.val)),
}
}
)

ModLeaSP = 'lea' 'q'? - a:AddrBP COMMA '%rsp' - {
mkcodedirective(".bundle_lock\n");
mkinsn("leal %s, %%esp\n", a.val);
mkinsn("orq %%r14, %%rsp\n");
mkcodedirective(".bundle_unlock\n");
}

ModImmSP = m:MODINST i:IMM COMMA '%rsp' - {
char* op = l(m.val);
mkcodedirective(".bundle_lock\n");
mkinsn("%s %s, %%esp\n", op, i.val);
mkinsn("orq %%r14, %%rsp\n");
mkcodedirective(".bundle_unlock\n");
tfree(m); tfree(i); free(op);
}

ModRegSP = m:MODINST r:XREG COMMA '%rsp' - {
char* op = l(m.val);
mkcodedirective(".bundle_lock\n");
mkinsn("%s %s, %%esp\n", op, lo(r.val));
mkinsn("orq %%r14, %%rsp\n");
mkcodedirective(".bundle_unlock\n");
tfree(m); tfree(r); free(op);
}

Expand Down Expand Up @@ -485,6 +513,10 @@ IMM = < IMM_RAW > - { $$ = (Transform) { .val = strndup(yytext, yyleng) } }

IMM_VAR = < ([-+a-zA-Z0-9_.@]+ | BALANCED_RAW) > - { $$ = (Transform) { .val = strndup(yytext, yyleng) } }

NUM = < (('0x' [0-9a-fA-F]+) | [0-9]+) > - {
$$ = (Transform) { .val = strndup(yytext, yyleng) };
}

IMM_RAW = (
('$' -)?
(
Expand Down Expand Up @@ -574,7 +606,7 @@ XREG = < (

ID = [a-zA-Z_.][-a-zA-Z0-9_.+]*

ITEM = < [^ ,;\n\r#/]+ > - { $$ = (Transform) { .val = strndup(yytext, yyleng) } }
ITEM = < [^ ,;\n\r#/()]+ > - { $$ = (Transform) { .val = strndup(yytext, yyleng) } }

COMMA = ',' -
EXCLAM = '!' -
Expand All @@ -592,9 +624,9 @@ EOL = '\n' | '\r\n' | '\r'
bool
lfigen()
{
// while (yyparse());
if (!yyparse())
return false;
while (yyparse());
//if (!yyparse())
// return false;

fprintf(output, ".bundle_align_mode 4\n");
struct op* op = ops;
Expand Down
8 changes: 8 additions & 0 deletions lfi-leg/out.txt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
lfi-amd64.leg: In function ‘yy_7_Addr’:
lfi-amd64.leg:324:10: error: expected ‘;’ before ‘tfree’
324 | }
| ^
| ;
325 | tfree(i);
| ~~~~~
Knitfile: 'lfi-leg-amd64': error during recipe: exit status 1
18 changes: 18 additions & 0 deletions lfi-leg/test/amd64/test.s
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,3 +36,21 @@ cmpl $44, 352(%rsp,%rax,4) # imm = 0x100
notrack jmp *%rax

callq *__cxa_finalize@GOTPCREL(%rip)

movq %rdi, 0x0

fldt 8(%rsp)

movl (%rdx,%rsi,4), %edx

orl $1, 12+__cpu_model(%rip)

jmp *(%rax)

callq *(%rax, %rdi, 4)

leaq -0x18(%rbp), %rsp

leaq -0x10(%rsp), %rsp

mov (,%rax,8),%rdx

0 comments on commit 2836fb4

Please sign in to comment.