diff options
| -rw-r--r-- | collect.c | 8 | ||||
| -rw-r--r-- | synth.py | 59 | ||||
| -rw-r--r-- | synth.zig | 82 |
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); } |