Read values from files

3 files changed, 76 insertions, 73 deletions

diff --git a/collect.c b/collect.c
index a092555..dc009f1 100644
--- a/collect.c
+++ b/collect.c
@@ -60,14 +60,6 @@ void log(const struct STATE *state)
 	static mutex_t mutex = MUTEX_INITIALIZER;
 	while (mutex_lock(&mutex) < 0);
 	write(output_file, (const char *)state, sizeof(struct STATE));
-	/*
-	 * struct STATE starts with a 16-bit member flags,
-	 * followed by 64-bit registers, leaving 6 bytes in between.
-	 */
-	const int offset = (int) sizeof(uint32_t) - (int) sizeof(struct STATE);
-	lseek(output_file, offset, SEEK_END);
-	write(output_file, (const char *)&stack_size, sizeof(uint32_t));
-	lseek(output_file, 0, SEEK_END);
 	write(output_file, (const char *)state->rsp, stack_size);
 	fsync(output_file);
 	mutex_unlock(&mutex);
diff --git a/synth.py b/synth.py
deleted file mode 100644
index 6779eb1..0000000
--- a/synth.py
+++ /dev/null
@@ -1,59 +0,0 @@
-#!/usr/bin/env python3
-# Patch's predicate synthesizer
-# Copyright (C) 2024-2025  Nguyễn Gia Phong
-#
-# This file is part of taosc.
-#
-# Taosc is free software: you can redistribute it and/or modify
-# it under the terms of the GNU Affero General Public License as published by
-# the Free Software Foundation, either version 3 of the License, or
-# (at your option) any later version.
-#
-# Taosc is distributed in the hope that it will be useful,
-# but WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-# GNU Affero General Public License for more details.
-#
-# You should have received a copy of the GNU Affero General Public License
-# along with taosc.  If not, see <https://www.gnu.org/licenses/>.
-
-from argparse import ArgumentParser
-from cProfile import run
-from functools import partial
-from pathlib import Path
-from sys import stderr
-
-from pacfix import learn
-from pacfix.invariant import INVARIANT_MAP, InvariantType
-from pacfix.utils import get_live_vars, get_valuations, parse_valuation
-
-write = partial(print, end='')
-
-
-def write_invariant(inv):
-    if inv.inv_type == InvariantType.VAR:
-        write('v')
-        write(inv.data)
-    elif inv.inv_type == InvariantType.CONST:
-        write('n' if inv.data < 0 else 'p')
-        write(abs(inv.data))
-    else:
-        write(INVARIANT_MAP[inv.inv_type])
-        write_invariant(inv.left)
-        write_invariant(inv.right)
-
-
-arg_parser = ArgumentParser(prog='taosc-synth')
-arg_parser.add_argument('input', help='input directory', type=Path)
-arg_parser.add_argument('delta', help='PAC delta', type=float,
-                        nargs='?', default=0.01)
-args = arg_parser.parse_args()
-
-with open(args.input / 'list') as f: live_vars = get_live_vars(f)
-vals_neg, vals_pos = parse_valuation(get_valuations(args.input / 'neg'),
-                                     get_valuations(args.input / 'pos'))
-result = learn(live_vars, vals_neg, vals_pos, args.delta)
-print('PAC epsilon:', result.pac_epsilon, file=stderr)
-for i in result.inv_mgr.invs:
-    write_invariant(i)
-    print()
diff --git a/synth.zig b/synth.zig
index 2914b6c..453cb46 100644
--- a/synth.zig
+++ b/synth.zig
@@ -16,12 +16,23 @@
 // You should have received a copy of the GNU Affero General Public License
 // along with taosc.  If not, see <https://www.gnu.org/licenses/>.
 
+const Allocator = std.mem.Allocator;
+const ArenaAllocator = std.heap.ArenaAllocator;
+const Dir = std.fs.Dir;
+const File = std.fs.File;
+const Reader = std.Io.Reader;
+const argsAlloc = std.process.argsAlloc;
+const argsFree = std.process.argsFree;
 const assert = std.debug.assert;
+const cwd = std.fs.cwd;
+const exit = std.process.exit;
+const page_allocator = std.heap.page_allocator;
+const parseUnsigned = std.fmt.parseUnsigned;
+const print = std.debug.print;
 const std = @import("std");
 
 const State = extern struct {
     flags: u16,
-    stack_size: u32,
     r15: i64,
     r14: i64,
     r13: i64,
@@ -37,13 +48,72 @@ const State = extern struct {
     rdx: i64,
     rcx: i64,
     rax: i64,
-    rsp: i64,
+    rsp: u64, // internal use only
     rip: i64,
 };
 
+fn countFiles(dir: Dir) Dir.Iterator.Error!usize {
+    var count: usize = 0;
+    var entries = dir.iterate();
+    while (try entries.next()) |entry| {
+        assert(entry.kind == .file);
+        count += 1;
+    }
+    return count;
+}
+
+const ReadError = Dir.Iterator.Error || File.OpenError || Reader.Error;
+
+const Data = struct {
+    states: []const State,
+    memory: []const u8,
+
+    fn init(allocator: Allocator, dir: Dir,
+            stack_len: u64) (Allocator.Error || ReadError)!Data {
+        const count = try countFiles(dir);
+        const states = try allocator.alloc(State, count);
+        const memory = try allocator.alloc(u8, stack_len * count);
+        var entries = dir.iterate();
+        var sp: u64 = 0;
+        for (states) |*state| {
+            const entry = try entries.next();
+            const file = try dir.openFile(entry.?.name, .{});
+            defer file.close();
+            var buffer: [4096]u8 = undefined;
+            var reader = file.reader(&buffer);
+            assert(try reader.read(@ptrCast(state)) == @sizeOf(State));
+            state.rsp = sp;
+            assert(try reader.read(memory[sp..][0..stack_len]) == stack_len);
+            sp += stack_len;
+            print("{}\n", .{ state });
+        }
+        return .{ .states = states, .memory = memory };
+    }
+
+    fn deinit(data: Data, allocator: Allocator) void {
+        allocator.free(data.states);
+        allocator.free(data.memory);
+    }
+};
+
 pub fn main() !void {
-    var reader = std.fs.File.stdin().reader(&.{});
-    var state: State = undefined;
-    assert(try reader.read(@ptrCast(&state)) == @sizeOf(State));
-    std.debug.print("{}\n", .{ state });
+    var arena = ArenaAllocator.init(page_allocator);
+    defer arena.deinit();
+    const allocator = arena.allocator();
+    const args = try argsAlloc(allocator);
+    defer argsFree(allocator, args);
+    if (args.len != 4) {
+        print("Usage: taosc-synth OFF-DIR ON-DIR STACK-SIZE", .{});
+        exit(1);
+    }
+    var off_dir = try cwd().openDir(args[1], .{ .iterate = true });
+    defer off_dir.close();
+    var on_dir = try cwd().openDir(args[2], .{ .iterate = true });
+    defer on_dir.close();
+    const stack_len = try parseUnsigned(u64, args[3], 0);
+
+    const off_data = try Data.init(allocator, off_dir, stack_len);
+    defer off_data.deinit(allocator);
+    const on_data = try Data.init(allocator, on_dir, stack_len);
+    defer on_data.deinit(allocator);
 }