souffle-lang / souffle

Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.
http://souffle-lang.github.io/
Universal Permissive License v1.0
916 stars 207 forks source link

Debug feature: live tracing of generated facts or dump facts to files after a specified number of iteration #2116

Open csabahruska opened 2 years ago

csabahruska commented 2 years ago

Hello,

It would be helpful to get feedback about the runtime behaviour of the fixed-point computation.

An example use case would be to provide fact data to debug a badly behaving points-to analysis implementation where the analysis can process small input but runs out of memory for large one. If I could observe the computed facts on the fly, then I could look for suspicious patterns in the data. But the facts will never be written out because the process will run out of memory before reaching the fixed-point.

Any of these would help me: 1) option to trace every new fact (print to stdout) 2) write out all output facts to the corresponding files after a given number of iterations

What do you think? Which approach is better and easier to implement?

Thanks, Csaba Hruska

b-scholz commented 2 years ago

I did this recently to debug subsumption. I've added print statements in the interpreter when new facts were produced for a relation.

The modification was pretty straightforward. I inserted at this point https://github.com/souffle-lang/souffle/blob/417b74a68679647081f7547cec330ef653fbfedb/src/interpreter/Engine.cpp#L1745 the following code fragment:

  std::cout << rel.getName() << ":";
  for(int i=0;i<arity; i++) { 
     std::cout << tuple[i] << " ";
  } 

The modification is a hack, and we would need to make it work for the compiler and interpreter using flags etc.

b-scholz commented 2 years ago

I forgot to mention that the tuple elements might be re-order. Don't get confused by this. If you do this for the synthesiser, you will see the tuple elements printed correctly.