Compile bdd to c

zyedidia · May 13, 2024 · 99e3055 · 99e3055
1 parent f3b8eda
commit 99e3055
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 24 deletions.
diff --git a/lfi-veribdd/generator/bdd.go b/lfi-veribdd/generator/bdd.go
@@ -42,8 +42,24 @@ func writeDot(nodes []Node, w io.Writer) {
 	fmt.Fprintln(w, "}")
 }
 
+func writeC(nodes []Node, w io.Writer) {
+	fmt.Fprintln(w, "static bool verify_insn(uint32_t insn) {")
+	fmt.Fprintf(w, "\tgoto node%d;\n", len(nodes)-1)
+	fmt.Fprintln(w, "node0: return false;")
+	fmt.Fprintln(w, "node1: return true;")
+	for i, n := range nodes[2:] {
+		fmt.Fprintf(w, "node%d:\n", i+2)
+		fmt.Fprintf(w, "\tif ((insn >> %d) & 0x1)\n", n.v)
+		fmt.Fprintf(w, "\t\tgoto node%d;\n", n.hi)
+		fmt.Fprintf(w, "\telse\n")
+		fmt.Fprintf(w, "\t\tgoto node%d;\n", n.lo)
+	}
+	fmt.Fprintln(w, "}")
+}
+
 func main() {
 	dot := flag.Bool("graph", false, "produce graphviz dot graph")
+	c := flag.Bool("c", false, "produce C code")
 
 	flag.Parse()
 	args := flag.Args()
@@ -87,6 +103,8 @@ func main() {
 
 	if *dot {
 		writeDot(nodes, os.Stdout)
+	} else if *c {
+		writeC(nodes, os.Stdout)
 	} else {
 		buf := &bytes.Buffer{}
 

diff --git a/lfi-veribdd/verifier.c b/lfi-veribdd/verifier.c
@@ -1,29 +1,7 @@
-#include "lfi.bdd.h"
-
 #include <stdint.h>
 #include <string.h>
 #include <stdbool.h>
 
-struct node {
-    uint8_t var;
-    uint16_t lo;
-    uint16_t hi;
-};
-
-static bool lookup(struct node* nodes, struct node* n, uint32_t val) {
-    uint8_t bit = (val >> n->var) & 1;
-    if (bit) {
-        if (n->hi < 2) return n->hi;
-        return lookup(nodes, &nodes[n->hi], val);
-    }
-
-    if (n->lo < 2) return n->lo;
-    return lookup(nodes, &nodes[n->lo], val);
-}
-
-static struct node* bdd_nodes = (struct node*) generator_lfi_bdd;
-static struct node* bdd_entry = &((struct node*) &generator_lfi_bdd)[(sizeof(generator_lfi_bdd) / sizeof(struct node)) - 1];
-
 #define X(x,y) x ## _ ## y
 #define XX(x,y) X(x,y)
 
@@ -33,8 +11,10 @@ static struct node* bdd_entry = &((struct node*) &generator_lfi_bdd)[(sizeof(gen
 #define EXPORT(a) XX(lfi, a)
 #endif
 
+#include "bdd.c"
+
 bool EXPORT(verify_insn)(uint32_t insn) {
-    return lookup(bdd_nodes, bdd_entry, insn);
+    return verify_insn(insn);
 }
 
 bool EXPORT(verify_bytes)(char* b, size_t size, void* error) {
@@ -43,7 +23,7 @@ bool EXPORT(verify_bytes)(char* b, size_t size, void* error) {
     uint32_t* insns = (uint32_t*) b;
 
     for (size_t i = 0; i < size / sizeof(uint32_t); i++) {
-        if (!lookup(bdd_nodes, bdd_entry, insns[i]))
+        if (!verify_insn(insns[i]))
             return false;
     }
     return true;