From 75d5b70e9791f46a74732c6ea5478399ad6bda11 Mon Sep 17 00:00:00 2001 From: Anastasios Antoniadis Date: Sat, 28 Dec 2024 18:27:33 +0200 Subject: [PATCH] Add hashsum functor with examples --- Makefile | 14 +- hashsum-example.dl | 19 ++ hashsum_functor.cpp | 36 +++ lub_functor.cpp | 39 ++++ tla-example-with-functor.dl | 363 ++++++++++++++++++++++++++++++ user-defined-aggregate-example.dl | 38 ++++ 6 files changed, 505 insertions(+), 4 deletions(-) create mode 100644 hashsum-example.dl create mode 100644 hashsum_functor.cpp create mode 100644 lub_functor.cpp create mode 100644 tla-example-with-functor.dl create mode 100644 user-defined-aggregate-example.dl diff --git a/Makefile b/Makefile index c5c4e81..c21b596 100644 --- a/Makefile +++ b/Makefile @@ -8,17 +8,23 @@ WORD_SIZE=32 # rudimentary all: libsoufflenum.so num_tests mappings_tests keccak256_tests -libsoufflenum.so: $(KECCAK_OBJ) num256.o mappings.o keccak256.o lists.o smt-api.o - g++ -std=c++17 -shared -o libsoufflenum.so $(KECCAK_OBJ) smt-api.o num256.o mappings.o keccak256.o lists.o -march=native -lz3 -fopenmp -DRAM_DOMAIN_SIZE=$(WORD_SIZE) +libsoufflenum.so: $(KECCAK_OBJ) num256.o mappings.o keccak256.o lists.o smt-api.o hashsum_functor.o lub_functor.o + g++ -std=c++17 -shared -o libsoufflenum.so $(KECCAK_OBJ) smt-api.o num256.o mappings.o keccak256.o lists.o hashsum_functor.o lub_functor.o -march=native -lz3 -fopenmp -DRAM_DOMAIN_SIZE=$(WORD_SIZE) ln -sf libsoufflenum.so libfunctors.so +hashsum_functor.o: hashsum_functor.cpp + g++ -std=c++17 hashsum_functor.cpp -lz3 -fopenmp -DRAM_DOMAIN_SIZE=$(WORD_SIZE) -c -fPIC -o hashsum_functor.o + +lub_functor.o: lub_functor.cpp + g++ -std=c++17 lub_functor.cpp -lz3 -fopenmp -DRAM_DOMAIN_SIZE=$(WORD_SIZE) -c -fPIC -o lub_functor.o + smt-api.o: smt-api.cpp - g++ -std=c++17 smt-api.cpp -lz3 -fopenmp -DRAM_DOMAIN_SIZE=$(WORD_SIZE) -c -fPIC -o smt-api.o + g++ -std=c++17 smt-api.cpp -lz3 -fopenmp -DRAM_DOMAIN_SIZE=$(WORD_SIZE) -c -fPIC -o smt-api.o num256.o: num256.cpp g++ -std=c++17 -O2 num256.cpp -c -fPIC -o num256.o -lz3 -fopenmp -num_tests: num256.cpp num256_test.cpp +num_tests: num256.cpp num256_test.cpp g++ -std=c++17 -o num_tests num256_test.cpp ./num_tests diff --git a/hashsum-example.dl b/hashsum-example.dl new file mode 100644 index 0000000..d5e39b7 --- /dev/null +++ b/hashsum-example.dl @@ -0,0 +1,19 @@ +.decl numbers(x:number) +.decl sum_result(x:number) +.decl hsum_result(x:number) +.output sum_result() +.output hsum_result() +.functor hashsum(i1:number, i2:number):number stateful + +numbers(-1). +numbers(1). +numbers(2). +numbers(3). +numbers(4). +numbers(5). + +sum_result(x) :- + x = sum a : { numbers(a), a > 0 }. + +hsum_result(x) :- + x = @@hashsum a : 0, { numbers(a), a > 0 }. diff --git a/hashsum_functor.cpp b/hashsum_functor.cpp new file mode 100644 index 0000000..738e749 --- /dev/null +++ b/hashsum_functor.cpp @@ -0,0 +1,36 @@ +#include "souffle/SouffleFunctor.h" +#include "souffle/utility/MiscUtil.h" +#include + +#if RAM_DOMAIN_SIZE == 64 +using FF_int = int64_t; +using FF_uint = uint64_t; +using FF_float = double; +#else +using FF_int = int32_t; +using FF_uint = uint32_t; +using FF_float = float; +#endif + +extern "C" { + souffle::RamDomain hashsum(souffle::SymbolTable* symbolTable, souffle::RecordTable* recordTable, + souffle::RamDomain arg1, souffle::RamDomain arg2); + unsigned long djb2(const std::string &str); +} + +souffle::RamDomain hashsum(souffle::SymbolTable* symbolTable, souffle::RecordTable* recordTable, souffle::RamDomain arg1, souffle::RamDomain arg2) { + assert(symbolTable && "NULL symbol table"); + assert(recordTable && "NULL record table"); + + std::string result = std::to_string(arg1 + djb2(std::to_string(arg2))); + return arg1 + djb2(std::to_string(arg2)); +} + +unsigned long djb2(const std::string &str) { + unsigned long hash = 5381; // Initialize hash with a prime number + for (char c : str) { + // Multiply hash by 33 and add the current character + hash = ((hash << 5) + hash) + c; // hash * 33 + c + } + return hash; +} \ No newline at end of file diff --git a/lub_functor.cpp b/lub_functor.cpp new file mode 100644 index 0000000..80e1e38 --- /dev/null +++ b/lub_functor.cpp @@ -0,0 +1,39 @@ +#include "souffle/SouffleFunctor.h" +#include "souffle/utility/MiscUtil.h" +#include + +#if RAM_DOMAIN_SIZE == 64 +using FF_int = int64_t; +using FF_uint = uint64_t; +using FF_float = double; +#else +using FF_int = int32_t; +using FF_uint = uint32_t; +using FF_float = float; +#endif + +extern "C" { +souffle::RamDomain lub(souffle::SymbolTable* symbolTable, souffle::RecordTable* recordTable, + souffle::RamDomain i1, souffle::RamDomain i2); +souffle::RamDomain lub_number(souffle::SymbolTable* symbolTable, souffle::RecordTable* recordTable, + souffle::RamDomain i, souffle::RamDomain x); +} + +souffle::RamDomain lub(souffle::SymbolTable*, souffle::RecordTable* recordTable, souffle::RamDomain i1, + souffle::RamDomain i2) { + const souffle::RamDomain* interval1 = recordTable->unpack(i1, 2); + const souffle::RamDomain* interval2 = recordTable->unpack(i2, 2); + auto lb = std::min(interval1[0], interval2[0]); + auto ub = std::max(interval1[1], interval2[1]); + const souffle::RamDomain res[2] = {lb, ub}; + return recordTable->pack(res, 2); +} + +souffle::RamDomain lub_number(souffle::SymbolTable*, souffle::RecordTable* recordTable, souffle::RamDomain i, + souffle::RamDomain x) { + const souffle::RamDomain* interval = recordTable->unpack(i, 2); + auto lb = std::min(interval[0], x); + auto ub = std::max(interval[1], x); + const souffle::RamDomain res[2] = {lb, ub}; + return recordTable->pack(res, 2); +} \ No newline at end of file diff --git a/tla-example-with-functor.dl b/tla-example-with-functor.dl new file mode 100644 index 0000000..67ee438 --- /dev/null +++ b/tla-example-with-functor.dl @@ -0,0 +1,363 @@ +.type ServerId <: symbol +.type ClientId <: symbol +.functor hashsum(i1:number, i2:number):number stateful + +/* + * Ordering predicates (scaffolding) + */ +.decl IsServer(id: ServerId) +.decl ServerLT(s1: ServerId, s2: ServerId) +ServerLT(s1, s2) :- + IsServer(s1), + IsServer(s2), + ord(s1) < ord(s2). + +.decl ServerIndex(s: ServerId, index: number) +ServerIndex(s, i) :- + IsServer(s), + i = count : ServerLT(_, s). + +.decl FirstServer(s: ServerId) +FirstServer(s) :- + IsServer(s), + !ServerLT(_, s). + +.decl LastServer(s: ServerId) +LastServer(s) :- + IsServer(s), + !ServerLT(s, _). + +.decl LastServerIndex(s: ServerId, index: number) +LastServerIndex(s, index) :- + LastServer(s), + ServerIndex(s, index). + +.decl NextServer(p: ServerId, n: ServerId) +NextServer(p, n) :- + ServerIndex(p, i), + ServerIndex(n, i+1). + +.decl NumServers(n: number) +NumServers(n+1) :- + LastServerIndex(_, n). + + +.decl IsClient(id: ClientId) +.decl ClientLT(c1: ClientId, c2: ClientId) +ClientLT(c1, c2) :- + IsClient(c1), + IsClient(c2), + ord(c1) < ord(c2). + +.decl ClientIndex(c: ClientId, index: number) +ClientIndex(c, i) :- + IsClient(c), + i = count : ClientLT(_, c). + +.decl FirstClient(c: ClientId) +FirstClient(c) :- + IsClient(c), + !ClientLT(_, c). + +.decl LastClient(c: ClientId) +LastClient(c) :- + IsClient(c), + !ClientLT(c, _). + +.decl LastClientIndex(c: ClientId, index: number) +LastClientIndex(c, index) :- + LastClient(c), + ClientIndex(c, index). + +.decl NextClient(p: ClientId, n: ClientId) +NextClient(p, n) :- + ClientIndex(p, i), + ClientIndex(n, i+1). + +.decl NumClients(n: number) +NumClients(n+1) :- + LastClientIndex(_, n). + + +// Similar ordering for client-server pairs +.decl ClientServerIndex(c: ClientId, s: ServerId, i: number) +ClientServerIndex(c, s, ci*ns + si) :- + ClientIndex(c, ci), + ServerIndex(s, si), + NumServers(ns). + + +/* + * Types + */ + +.type Action = [ + kind : symbol, // "connect" or "disconnect" + clientId : ClientId, + serverId : ServerId +] + +.type LockedState = [ + serverIndex: number, + rest: LockedState +] + +.type HeldState = [ + clientServerIndex: number, + rest: HeldState +] + +.type State = [ + locked: LockedState, + held: HeldState +] + + +.decl DecomposeAction(a: Action, k: symbol, c: ClientId, s: ServerId) +DecomposeAction(a, k, c, s) :- + IsClient(c), + IsServer(s), + (k = "connect"; k = "disconnect"), + a = [k, c, s]. + + + +// Single transition component +.comp Transition { + /* + * Main state predicates + */ + .decl Locked(state: State, server: ServerId) + .decl Locked_Prime(prevState: State, action: Action, server: ServerId) + .decl Locked_Prime_Index(prevState: State, action: Action, si: number) + + // client holds server + .decl Held(state: State, client: ClientId, server: ServerId) + .decl Held_Prime(prevState: State, action: Action, client: ClientId, server: ServerId) + .decl Held_Prime_Index(prevState: State, action: Action, csi: number) + + .decl IsState(state: State) + IsState(state) :- + (Locked(state, _); + Held(state, _, _)), + state != nil. + + Locked_Prime_Index(prevState, action, si) :- + Locked_Prime(prevState, action, server), + ServerIndex(server, si). + + Held_Prime_Index(prevState, action, csi) :- + Held_Prime(prevState, action, client, server), + ClientServerIndex(client, server, csi). + + + /* + * Forall iterations, in order to finalize the state. Scaffolding, not essential logic. + */ + + .decl PossibleAction(prevState: State, action: Action) + PossibleAction(prevState, action) :- + ConnectPossibleAction(prevState, action); + DisconnectPossibleAction(prevState, action). + + .decl HeldStateUpTo(prevState: State, action: Action, clientServerIndex: number, partialState: HeldState) + HeldStateUpTo(prevState, action, index, [index, nil]) :- + PossibleAction(prevState, action), + index = @@hashsum i: 0, {Held_Prime_Index(prevState, action, i)}. + +// HeldStateUpTo(prevState, action, nextIndex, [nextIndex, prevPartialState]) :- +// HeldStateUpTo(prevState, action, prevIndex, prevPartialState), +// nextIndex = min(i): { +// Held_Prime_Index(prevState, action, i), +// i > prevIndex +// }. + + .decl LockedStateUpTo(prevState: State, action: Action, si: number, partialState: LockedState) + LockedStateUpTo(prevState, action, index, [index, nil]) :- + PossibleAction(prevState, action), + index = @@hashsum i: 0, {Locked_Prime_Index(prevState, action, i)}. + +// LockedStateUpTo(prevState, action, nextIndex, [nextIndex, prevPartialState]) :- +// LockedStateUpTo(prevState, action, prevIndex, prevPartialState), +// nextIndex = min(i): { +// Locked_Prime_Index(prevState, action, i), +// i > prevIndex +// }. + + .decl HeldStateFinalized(prevState: State, action: Action, hstate: HeldState) + HeldStateFinalized(prevState, action, state) :- + HeldStateUpTo(prevState, action, maxIndex, state), + maxIndex = @@hashsum i: 0, {Held_Prime_Index(prevState, action, i)}. + + HeldStateFinalized(prevState, action, nil) :- + PossibleAction(prevState, action), + !Held_Prime_Index(prevState, action, _). + + .decl LockedStateFinalized(prevState: State, action: Action, lstate: LockedState) + LockedStateFinalized(prevState, action, state) :- + LockedStateUpTo(prevState, action, maxIndex, state), + maxIndex = @@hashsum i: 0, {Locked_Prime_Index(prevState, action, i)}. + + LockedStateFinalized(prevState, action, nil) :- + PossibleAction(prevState, action), + !Locked_Prime_Index(prevState, action, _). + + .decl TotalStateFinalized(state: State, prevState: State, action: Action) + TotalStateFinalized([ls, hs], prevState, action) :- + HeldStateFinalized(prevState, action, hs), + LockedStateFinalized(prevState, action, ls). + + + /* + * Optimization predicates capturing just the "not equals" relation + */ + + .decl NotSameServer(s1: ServerId, s2: ServerId) + NotSameServer(s1, s2) :- + IsServer(s1), + IsServer(s2), + s1 != s2. + + .decl NotSameClient(c1: ClientId, c2: ClientId) + NotSameClient(c1, c2) :- + IsClient(c1), + IsClient(c2), + c1 != c2. + + + /* + * Transition rules for next state + */ + + // Auxiliary predicates, both for optimization and used elsewhere + .decl ConnectPossible(prevState: State, c: ClientId, s: ServerId, action: Action) + ConnectPossible(prevState, c, s, action) :- + Locked(prevState, s), + DecomposeAction(action, "connect", c, s). + + .decl ConnectPossibleAction(prevState: State, action: Action) + ConnectPossibleAction(prevState, action) :- + ConnectPossible(prevState, _, _, action). + + // What happens to Held, upon a connect + Held_Prime(prevState, action, c2, s2) :- + ConnectPossibleAction(prevState, action), + Held(prevState, c2, s2). + + Held_Prime(prevState, action, c, s) :- + ConnectPossible(prevState, c, s, action). + + // Locked, upon a connect + Locked_Prime(prevState, action, s2) :- + ConnectPossible(prevState, _, s, action), + Locked(prevState, s2), + NotSameServer(s, s2). + + + // Optimization predicates + .decl DisconnectPossible(prevState: State, c: ClientId, s: ServerId, action: Action) + DisconnectPossible(prevState, c, s, action) :- + Held(prevState, c, s), + DecomposeAction(action, "disconnect", c, s). + + .decl DisconnectPossibleAction(prevState: State, action: Action) + DisconnectPossibleAction(prevState, action) :- + DisconnectPossible(prevState, _, _, action). + + // What happens to Held, upon a disconnect + Held_Prime(prevState, action, c2, s2) :- + DisconnectPossible(prevState, c, s, action), + Held(prevState, c2, s2), + (NotSameClient(c, c2); + NotSameServer(s, s2)). + + // Locked, upon a disconnect + Locked_Prime(prevState, action, s2) :- + DisconnectPossibleAction(prevState, action), + Locked(prevState, s2). + + Locked_Prime(prevState, action, s) :- + DisconnectPossible(prevState, _, s, action). + + .output IsState +} // end of Transition component + + +.init T1 = Transition +.init T2 = Transition +.init T3 = Transition +.init T4 = Transition +.init T5 = Transition +.init T6 = Transition +.init T7 = Transition +.init TFinal = Transition + +/* + * Initial state (successor of nil) + */ + +// Initial state is nil +T1.Locked(nil, s) :- + IsServer(s). + + +/* + * Connecting transitions + */ + +#define CopyRelations(tNew, tOld) \ + tNew.Held(state, client, server) :- tOld.Held(state, client, server). \ + tNew.Locked(state, server) :- tOld.Locked(state, server). \ + tNew.Held(state, client, server) :- tOld.TotalStateFinalized(state, prevState, action), tOld.Held_Prime(prevState, action, client, server). \ + tNew.Locked(state, server) :- tOld.TotalStateFinalized(state, prevState, action), tOld.Locked_Prime(prevState, action, server). + + // tNew.Held_Prime(state, action, client, server) :- tOld.Held_Prime(state, action, client, server). \ + // tNew.Held_Prime_Index(state, action, csi) :- tOld.Held_Prime_Index(state, action, csi). \ + // tNew.Locked_Prime(state, action, server) :- tOld.Locked_Prime(state, action, server). \ + // tNew.Locked_Prime_Index(state, action, si) :- tOld.Locked_Prime_Index(state, action, si). \ + // tNew.HeldStateUpTo(prevState, action, clientServerIndex, partialState) :- tOld.HeldStateUpTo(prevState, action, clientServerIndex, partialState). \ + // tNew.LockedStateUpTo(prevState, action, si, partialState) :- tOld.LockedStateUpTo(prevState, action, si, partialState). \ + +CopyRelations(T2, T1) +CopyRelations(T3, T2) +CopyRelations(T4, T3) +CopyRelations(T5, T4) +CopyRelations(T6, T5) +CopyRelations(T7, T6) +CopyRelations(TFinal, T7) + + +.decl Unsafe(state: State, c1: ClientId, c2: ClientId) +Unsafe(state, c1, c2) :- + TFinal.Held(state, c1, s), + TFinal.Held(state, c2, s), + c1 != c2. + + +/* + * Setup of problem instance + */ + +IsServer("a"). +IsServer("b"). +IsServer("c"). +IsServer("d"). +IsServer("e"). +IsServer("f"). +IsServer("g"). +IsClient("1"). +IsClient("2"). +IsClient("3"). +IsClient("4"). +IsClient("5"). +IsClient("6"). +IsClient("7"). + +// .printsize Locked +// .printsize Held + + +.printsize TFinal.IsState + +// .output IsState +.output Unsafe \ No newline at end of file diff --git a/user-defined-aggregate-example.dl b/user-defined-aggregate-example.dl new file mode 100644 index 0000000..62505ed --- /dev/null +++ b/user-defined-aggregate-example.dl @@ -0,0 +1,38 @@ +// Souffle - A Datalog Compiler +// Copyright (c) 2022, The Souffle Developers. All rights reserved +// Licensed under the Universal Permissive License v 1.0 as shown at: +// - https://opensource.org/licenses/UPL +// - /licenses/SOUFFLE-UPL.txt + +.type AbstractValue = [lb:number, ub:number] + +// builds the AbstractValues [0, 1], [1, 2], ... [999, 1000] +.decl A(i:AbstractValue) +A([x,x+1]) :- x = range(0, 1000). + +.functor lub(i1:AbstractValue, i2:AbstractValue):AbstractValue stateful + + +.decl B(i:AbstractValue) +.output B + +/* +res = [0,0] +for (x s.t A(x)) { + res = @lub(res, x); +} +insert res into B +*/ +B(i) :- + i = @@lub x : [0,0], {A(x)}. + +.functor lub_number(i1:AbstractValue, x:number):AbstractValue stateful + +.decl N(x:number) +N(x) :- x = range(0, 1000). + +.decl C(i:AbstractValue) +.output C + +C(i) :- + i = @@lub_number x : [0,0], {N(x)}. \ No newline at end of file