File

module binary_input_file(data,cont) = {
    action write(d:data)
    action read returns (d:data)
    action sync(c:cont)
    action synced(c:cont)

    specification {
        var contents : data
        relation pending(C:cont)

        after init {
            pending(C) := false;
        }

        before write {
            contents := d;
        }

        after read {
            ensure d = contents;

<<< std::cerr << d << std::endl; //std::cerr << contents << std::endl;

        }

        before sync {
            require ~pending(c);
            pending(c) := true;
        }

        before synced {
            require pending(c);
            pending(c) := false;
        }
    }

    implementation {
        object fildes = {}
        <<< member
            int `fildes`;
        >>>
        <<< init
            {
        std::string pathname = "`this`.txt";
        std::string pathname2;
        std::cerr << pathname << std::endl;
        const char * session_file = getenv("PROOTPATH");
        if(session_file != NULL) {
            std::cerr << "PROOTPATH 5b " << session_file<< "\n";
            pathname2 += session_file;
            pathname2 += "/";

            // Use simplified PANTHER_IVY_BASE_DIR approach
            const char* base_dir = getenv("PANTHER_IVY_BASE_DIR");
            if (base_dir) {
                std::cerr << "PANTHER_IVY_BASE_DIR 5b " << base_dir << "\n";
                pathname2 = base_dir;
            } else {
                // Fallback for backward compatibility
                std::cerr << "Using default PANTHER_IVY_BASE_DIR\n";
                pathname2 += "panther_ivy/protocol-testing/quic";
            }
            pathname2 += "/quic_utils/";
            pathname = pathname2 + pathname;
            std::cerr << pathname << std::endl;
        } else {
            char * session_file2 = getenv("IVY_INCLUDE_PATH");
            pathname = session_file2 + pathname; //TODO fix, for namespace, else bug
        }
        std::cerr << pathname << std::endl;
        int f = ::open(pathname.c_str(),O_RDWR,0666);
        if (f < 0) {
            perror("cannot open file");
        }
        `fildes` = f;
        std::cerr << `fildes` << std::endl;

        }
        >>>
        implement write {
        <<<
            std::cerr << "SWAG" << std::endl;
            std::cerr << `fildes` << std::endl;
            if (::lseek(`fildes`,0,SEEK_SET) < 0) {
                perror("cannot seek to beginning of file");
            }
            vector<unsigned char> bytes;
            bytes.resize(d.size());
            std::copy(d.begin(),d.end(),bytes.begin());
            if (::write(`fildes`,&bytes[0],bytes.size()) < 0) {
                perror("cannot seek to beginning of file");
            }
            if (::ftruncate(`fildes`,sr.res.size()) < 0) {
                perror("cannot truncate file");
            }
        >>>
        }
        implement read {
        <<<
            std::cerr << "COUCOU" << std::endl;
            if (::lseek(`fildes`,0,SEEK_SET) < 0) {
                perror("cannot seek to beginning of file");
            }
            std::vector<char> buf;
            ivy_socket_deser_128 ds(`fildes`,buf);  // initializer deserializer with zero bytes
            //ivy_socket_deser ds(`fildes`,buf);    // initializer deserializer with zero bytes
            while (ds.more(1)) {
                //long long res;
                int128_t res;
                ds.getn(res,1);
                d.push_back(res);
                std::cerr << d << std::endl;
                //std::cerr << contents << std::endl;
            }  // read all the bytes
            std::cerr << d << std::endl;
            //std::cerr << contents << std::endl;
        >>>
        }
        <<< impl
            template<typename cont, typename cbtype> class sync_reader : public reader {
                cont c;
                cbtype cb;
                int fd;
                ivy_class *ivy;
            public:
                sync_reader(cont c, int fd, cbtype cb, ivy_class *ivy) : c(c), fd(fd), cb(cb), ivy(ivy) {}
                int fdes() {return fd;}
                void read() {
                    ivy->__lock();
                    if (::fsync(fd) < 0)
                        { perror("failed to sync file"); }
                    fd = -1;
                    cb(c);
                    ivy->__unlock();
                }
            };
        >>>
        implement sync {
        <<<
            install_reader(new sync_reader<`cont`,%`synced`>(c,`fildes`,`synced`, this));
        >>>
        }
        action handle_synced(c:cont) = {
            call synced(c)
        }

    }
    trusted isolate iso = this
}