vmware / differential-datalog

DDlog is a programming language for incremental computation. It is well suited for writing programs that continuously update their output in response to input changes. A DDlog programmer does not write incremental algorithms; instead they specify the desired input-output mapping in a declarative manner.
MIT License
1.37k stars 117 forks source link

souffle's ord() is different from ddlog #1115

Closed Price1999a closed 2 years ago

Price1999a commented 2 years ago

tools/souffle_converter.py

The semantics of the ord() function is different in the two tools, but the conversion script does not prompt this, and directly converts it, which leads to potential bugs. Hope the script can throw an exception when it encounters this situation.

Price1999a commented 2 years ago

Due to my misunderstanding of the document, I need to change the problem description: tools/souffle_converter.py cannot convert the ord() function in souffle correctly, The ord() function in /lib/souffle_lib.dl is a Tsymble (IString) to Tnumber conversion, but souffle_converter.py does not handle this.

I personally made the following changes:

    def convert_function_call(self, function: parglare.NodeNonTerm) -> str:
        """Convert a call to a function"""
        # print(function.tree_str())
        func = self.get_function_name(function)
        args = getListField(function, "Arg", "FunctionArgumentList")
        argStrings = [self.convert_arg(arg) for arg in args]
        if func == "match":
            # Match is reserved keyword in DDlog
            func = "re_match"
        # Some functions like min, max, cat can be called with any number of arguments
        if func == "min" or func == "max" or func == "cat":
            if len(argStrings) == 0:
                raise Exception("Too few arguments for " + func)
            else:
                result = argStrings[0]
                del argStrings[0]
                for e in argStrings:
                    result = func + "(" + result + ", " + e + ")"
                return result
        if func == "to_unsigned":
            if self.currentType == "Tfloat":
                func = "ftou"
            else:
                # Guessing that the input is a number... we could be wrong
                func = "itou"
            self.setCurrentType("Tunsigned")
        elif func == "to_float":
            if self.currentType == "Tunsigned":
                func = "utof"
            else:
                # Assume it's a number...
                func = "itof"
            self.setCurrentType("Tfloat")
        elif func == "to_number":
            if self.currentType == "Tstring":
                func = "to_number"
            elif self.currentType == "Tfloat":
                func = "ftoi"
            elif self.currentType == "Tunsigned":
                func = "utoi"
            self.setCurrentType("Tnumber")
        elif func == "to_string":
            func = "to_istring"
            self.setCurrentType("Tstring")
        elif func == "ord":                                 //edit point
            self.setCurrentType("Tnumber")
        elif func == "range":
            if len(argStrings) == 2:
                argStrings.append("1")
            if len(argStrings) != 3:
                raise Exception("Expected 'range' to have 2 or 3 arguments")
            self.setCurrentType("Tnumber")
            return "FlatMap(range_vec(" + ", ".join(argStrings) + "))"
        return func + "(" + ", ".join(argStrings) + ")"

In addition, the way the new version of doop organizes facts files has changed, so there is also a small change in process_input: for directory in ["./", "./database/", "./facts/"]:

Price1999a commented 2 years ago

In fact, tools/.py cannot effectively process the output declaration of comp when converting facts (it is possible to convert logic). Based on the above questions, I made a modification to it:

    def process(self, tree: parglare.NodeNonTerm) -> None:
        decls = getListField(tree, "Declaration", "DeclarationList")
        for decl in decls:
            if self.conversion_options.skip_logic:
                self.process_only_facts(decl)
            else:
                self.process_decl(decl)
        self.files.output(self.aggregates)

    def preprocess(self, tree: parglare.NodeNonTerm) -> None:
        decls = getListField(tree, "Declaration", "DeclarationList")
        for decl in decls:
            # if self.conversion_options.skip_logic:
            #     self.process_only_facts(decl)
            # else:
            self.process_decl(decl)
        self.files.output(self.aggregates)

def convert(inputName: str, outputPrefix: str, options: ConversionOptions, debug=False) -> None:
    Type.clear()
    Relation.clear()
    if options.relationPrefix != "":
        assert options.relationPrefix.endswith("::"), "prefix is expected to end with a dot"
    files = Files(options, inputName, outputPrefix)
    parser = getParser(debug)
    tree: parglare.NodeNonTerm = parser.parse_file(files.inputName)
    converter = SouffleConverter(files, options)
    converter.preprocessing = True
    converter.preprocess(tree)

    # print("=================== finished preprocessing")
    converter.preprocessing = False
    converter.process(tree)
    files.done(Relation.dumpOrder)

souffle_converter.zip

I use the above file to test the script. The 2-object-sensitive+heap.dl here comes from a small change in the rules in Doop

mihaibudiu commented 2 years ago

Thank you for your bug reports. First, you should know that we don't keep track of the latest changes in Souffle, because they move quickly and break things too often. Our test script is pinned to an older release of theirs. Second, you should know that there are quite a few things in Souffle that we don't handle at all. They are on the "would be nice to do" list, but so are many other things. Some thing may never be fixable, since we disagree with some Souffle choices (for example, we think that group-by should never create empty groups...) However, we are not opposed to bringing it up-to-date. If you have fixed the translator, why not submit a pull request with your fixes?

mihaibudiu commented 2 years ago

Can we close this issue?