search

GaloisInc / cclyzerpp

cclyzer++ is a precise and scalable pointer analysis for LLVM code.
https://galoisinc.github.io/cclyzerpp/
BSD 3-Clause "New" or "Revised" License
137 stars 14 forks source link

Warnings when building with latest version of souffle #141

Closed mingodad closed 2 years ago

mingodad commented 2 years ago

When trying to build with the latest version of souffle I'm getting this warnings:

make
[  1%] Generating unification.cpp
Warning: No rules/facts defined for relation atomic_operation_fadd in atomicrmw-instr.dl:53:7
Warning: No rules/facts defined for relation atomic_operation_fsub in atomicrmw-instr.dl:54:7
Warning: Variable ?tailHead only occurs once in interface.dl:54:18
Warning: Variable ?alloc only occurs once in interface.dl:198:14
Warning: Variable ?z only occurs once in unification.dl:274:47
[  3%] Generating debug.cpp
Warning: No rules/facts defined for relation atomic_operation_fadd in atomicrmw-instr.dl:53:7
Warning: No rules/facts defined for relation atomic_operation_fsub in atomicrmw-instr.dl:54:7
Warning: Variable ?tailHead only occurs once in interface.dl:54:18
Warning: Variable ?alloc only occurs once in interface.dl:198:14
Warning: Variable ?z only occurs once in unification.dl:274:47
[  5%] Generating subset.cpp
Warning: No rules/facts defined for relation atomic_operation_fadd in atomicrmw-instr.dl:53:7
Warning: No rules/facts defined for relation atomic_operation_fsub in atomicrmw-instr.dl:54:7
Warning: Variable ?tailHead only occurs once in interface.dl:54:18
Warning: Variable ?alloc only occurs once in interface.dl:198:14

Souffle version:

Version: 2.3-137-gf2f974194
Word size: 32 bits
Options enabled: ffi openmp ncurses sqlite zlib
mingodad commented 2 years ago

Also I'm getting lots of link time errors like:

...
subset.cpp:(.text+0x5f220): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::insert(int, int, int)'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2ce760): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::contains(std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const':
subset.cpp:(.text+0x5f260): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::contains(std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2ce7a0): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::contains(std::array<int, 3ul> const&) const':
subset.cpp:(.text+0x5f2a0): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::contains(std::array<int, 3ul> const&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2ce7e0): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::size() const':
subset.cpp:(.text+0x5f2f0): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::size() const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2ce830): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::find(std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const':
subset.cpp:(.text+0x5f310): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::find(std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2ce850): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::find(std::array<int, 3ul> const&) const':
subset.cpp:(.text+0x5f360): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::find(std::array<int, 3ul> const&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2ce8a0): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_000(std::array<int, 3ul> const&, std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const':
subset.cpp:(.text+0x5f3d0): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_000(std::array<int, 3ul> const&, std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2ce910): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_000(std::array<int, 3ul> const&, std::array<int, 3ul> const&) const':
subset.cpp:(.text+0x5f440): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_000(std::array<int, 3ul> const&, std::array<int, 3ul> const&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2ce980): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_001(std::array<int, 3ul> const&, std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const':
subset.cpp:(.text+0x5f4b0): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_001(std::array<int, 3ul> const&, std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2ce9f0): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_001(std::array<int, 3ul> const&, std::array<int, 3ul> const&) const':
subset.cpp:(.text+0x5f590): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_001(std::array<int, 3ul> const&, std::array<int, 3ul> const&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cead0): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_100(std::array<int, 3ul> const&, std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const':
subset.cpp:(.text+0x5f610): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_100(std::array<int, 3ul> const&, std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2ceb50): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_100(std::array<int, 3ul> const&, std::array<int, 3ul> const&) const':
subset.cpp:(.text+0x5f700): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_100(std::array<int, 3ul> const&, std::array<int, 3ul> const&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cec40): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_110(std::array<int, 3ul> const&, std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const':
subset.cpp:(.text+0x5f780): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_110(std::array<int, 3ul> const&, std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cecc0): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_110(std::array<int, 3ul> const&, std::array<int, 3ul> const&) const':
subset.cpp:(.text+0x5f870): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_110(std::array<int, 3ul> const&, std::array<int, 3ul> const&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cedb0): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_111(std::array<int, 3ul> const&, std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const':
subset.cpp:(.text+0x5f8f0): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_111(std::array<int, 3ul> const&, std::array<int, 3ul> const&, souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::context&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cee30): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_111(std::array<int, 3ul> const&, std::array<int, 3ul> const&) const':
subset.cpp:(.text+0x5fa90): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::lowerUpperRange_111(std::array<int, 3ul> const&, std::array<int, 3ul> const&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cefd0): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::empty() const':
subset.cpp:(.text+0x5fb10): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::empty() const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cf050): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::partition() const':
subset.cpp:(.text+0x5fb40): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::partition() const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cf080): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::purge()':
subset.cpp:(.text+0x5fb80): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::purge()'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cf0c0): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::begin() const':
subset.cpp:(.text+0x5fbb0): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::begin() const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cf0f0): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::end() const':
subset.cpp:(.text+0x5fbf0): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::end() const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cf130): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::printStatistics(std::ostream&) const':
subset.cpp:(.text+0x5fc30): multiple definition of `souffle::t_btree_iii__2__0_1_2__001__100__110__111::Type::printStatistics(std::ostream&) const'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cf170): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__0_2_1__101__111::Type::insert(std::array<int, 3ul> const&)':
subset.cpp:(.text+0x5fc90): multiple definition of `souffle::t_btree_iii__0_2_1__101__111::Type::insert(std::array<int, 3ul> const&)'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cfa70): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__0_2_1__101__111::Type::insert(std::array<int, 3ul> const&, souffle::t_btree_iii__0_2_1__101__111::Type::context&)':
subset.cpp:(.text+0x5fcd0): multiple definition of `souffle::t_btree_iii__0_2_1__101__111::Type::insert(std::array<int, 3ul> const&, souffle::t_btree_iii__0_2_1__101__111::Type::context&)'
CMakeFiles/SoufflePAObject.dir/debug.cpp.o:debug.cpp:(.text+0x2cfab0): first defined here
CMakeFiles/SoufflePAObject.dir/subset.cpp.o: In function `souffle::t_btree_iii__0_2_1__101__111::Type::insert(int const*)':
...
langston-barrett commented 2 years ago

Hi @mingodad, thanks for the report!

I'm getting this warnings

Some of these warnings are expected, unfortunately. This comment explains one of them:

https://github.com/GaloisInc/cclyzerpp/blob/c8a24dc41d3329fe9f48d0f32dd6efa86eb2568b/datalog/context/interface.dl#L52-L55

For the unexpected ones, I've created #142.

Also I'm getting lots of link time errors like:

Are these fixed by #140?

Also, can you please say more about how you're building cclyzer++? Are you using the cclyzer-dev Docker image, or building on your host? What compiler are you using?

For what it's worth, the CI system builds cclyzer++ against Souffle 2.3. How did you build/install Souffle? I can't find revision gf2f974194 in the Souffle git history.

mingodad commented 2 years ago

I'm building on my host Ubuntu 18.04 with clang-14 and my build of souffle:

Version: 2.3-137-gf2f974194
Word size: 32 bits
Options enabled: ffi openmp ncurses sqlite zlib

The https://github.com/GaloisInc/cclyzerpp/pull/140 fix was not for the duplicated link errors.

langston-barrett commented 2 years ago

Okay, thanks! cclyzer++ has only really been tested on Ubuntu 20.04 and 22.04, but I don't think that should be a problem.

my build of souffle:

This seems like it might be the issue. Can you try with the official package from the PPA? See here for how to install it: https://souffle-lang.github.io/install. You could also try building cclyzer++ in the cclyzerpp-dev Docker image, which has the official build of Souffle 2.3 installed already:

docker pull ghcr.io/galoisinc/cclyzerpp-dev:main
docker run --rm -it ghcr.io/galoisinc/cclyzerpp-dev
rm -rf build
cmake -S . -B build -G Ninja
cmake --build build -j $(nproc)

Alternatively, if you just want to try cclyzer++, you could try just building the FactGenerator:

cmake --build build -j $(nproc) --target factgen-exe

Then you could run the analysis via the Souffle interpreter:

Finally, you could consider downloading a Debian/Ubuntu package from the releases page or running the cclyzerpp-dist Docker image.

Hope one of these options works for you!

mingodad commented 2 years ago

Thank you for all your help ! I just build an exact souffle-2.3 and now it builds.

This is my shell script used to configure the buidl:

#!/bin/sh
BOOSTPREFIX=$HOME/local/boost
SOUFFLEPREFIX=$HOME/local/souffle-2.3
export LD_LIBRARY_PATH=$BOOSTPREFIX/stage/lib:$LD_LIBRARY_PATH
export CLANG_HOME=$HOME/local/clang-14
export PATH=$CLANG_HOME/bin:$PATH
I$HOME/local/include"
export CC=clang
export CXX=clang++
export LLVM_ROOT_DIR=$CLANG_HOME
export CLANG_ROOT_DIR=$CLANG_HOME

mycmake -DSOUFFLE_INCLUDE=$SOUFFLEPREFIX/include -DBOOST_ROOT=$BOOSTPREFIX -DCMAKE_INSTALL_PREFIX=$HOME/local/cclyzerpp ..
langston-barrett commented 2 years ago

@mingodad Glad it worked out! I'll close this for now, but feel free to re-open if you have any further questions, or to start a discussion here: https://github.com/GaloisInc/cclyzerpp/discussions

mingodad commented 2 years ago

Looking at the link time problem I noticed that debug.project, subset.project and unification.project are almost the same with bit of unique code in each one. I did a small Lua script to create an amalgamation of then (the preprocessor can do it but the comments are eliminated), it can make easier to view the whole program and navigate through it.

local included = {}
local include_count = 0
local include_dup = {}
local include_dup_count = 0
local inc_sys = {}
local inc_sys_count = 0
local out = io.stdout

function CopyWithInline(prefix, filename)
    local full_path = prefix .. filename
    if included[full_path] then
        include_dup_count = include_dup_count + 1
        include_dup[full_path] = include_dup_count
        return
    end
    include_count = include_count + 1
    included[full_path] = include_count
    print('//--Start of', full_path);
    --if(filename:match("luac?.c"))
    local inp = assert(io.open(prefix .. filename, "r"))
    for line in inp:lines() do
        if line:match('#define LUA_USE_READLINE') then
            out:write("//" .. line .. "\n")
        else
            local inc = line:match('#include%s+(["<].-)[">]')
            if inc  then
                out:write("//" .. line .. "\n")
                if inc:sub(1,1) == '"' then
                    local nfname = inc:sub(2)
                    local eprefix = nfname:match("(.-/)[^/]+$")
                    --print("=1=", eprefix, nfname)
                    if eprefix then
                        nfname = nfname:sub(#eprefix+1)
                        eprefix = prefix .. eprefix
                    else
                        eprefix = prefix
                    end
                    --print("=2=", eprefix, nfname)
                    CopyWithInline(eprefix, nfname)
                else
                    local fn = inc:sub(2)
                    if inc_sys[fn] == null then
                        inc_sys_count = inc_sys_count +1
                        inc_sys[fn] = inc_sys_count
                    end
                end
            else
                out:write(line .. "\n")
            end
        end
      end
    print('//--End of', full_path);
end

--CopyWithInline('./', "debug.project");
--CopyWithInline('./', "subset.project");
--CopyWithInline('./', "unification.project");

function showIncludes(itbl, tname)
    print("//\n//\t".. tname .. "\n//")
    print("/*")
    local ordered_include = {}
    for k, v in pairs(itbl) do ordered_include[v] = k  end
    for k, v in ipairs(ordered_include) do print("#include <" .. v .. "> // " .. k ) end
    print("*/")
end

if #arg > 0 then
    CopyWithInline('./', arg[1]);
    showIncludes(included, "included files list");
    if #include_dup > 0 then
        showIncludes(include_dup, "include_dup");
    end
else
    print("usage:", arg[0], "project.filename")
end

To make an amalgamation save the above on datalog folder and use like this:

lua mk-amalgamation.lua debug.project > debug.project.dl

Here is a snippet of the results:

//--Start of    ./debug.project
//#include "subset-and-unification.project"
//--Start of    ./subset-and-unification.project
//#include "common.project"
//--Start of    ./common.project
//#include "schema/schema.project"
//--Start of    ./schema/schema.project
//#include "debug.dl"
//--Start of    ./schema/debug.dl
.type File <: symbol
.type Line <: number

// When true, this predicate enables all sanity checks of the project.
.decl schema_sanity()
//--End of  ./schema/debug.dl
//#include "calling-convention.dl"
//--Start of    ./schema/calling-convention.dl
// http://llvm.org/docs/LangRef.html#callingconv
// keywords: funcstruction; call_instr; invoke_instr

.type CallingConvention <: symbol
.decl calling_convention(conv:CallingConvention)

.decl fast_calling_convention(conv:CallingConvention)
.decl cold_calling_convention(conv:CallingConvention)
.decl x86_fastcall_calling_convention(conv:CallingConvention)
.decl x86_stdcall_calling_convention(conv:CallingConvention)
.decl x86_thiscall_calling_convention(conv:CallingConvention)
.decl intel_ocl_bi_calling_convention(conv:CallingConvention)
.decl arm_aapcs_calling_convention(conv:CallingConvention)
.decl arm_aapcs_vfp_calling_convention(conv:CallingConvention)
.decl arm_apcs_calling_convention(conv:CallingConvention)
.decl msp430_intr_calling_convention(conv:CallingConvention)
.decl ptx_device_calling_convention(conv:CallingConvention)
.decl ptx_kernel_calling_convention(conv:CallingConvention)
...
ptx_device_calling_convention("ptx_device").
ptx_kernel_calling_convention("ptx_kernel").
//--End of  ./schema/calling-convention.dl
//#include "ordering.dl"
//--Start of    ./schema/ordering.dl
// Ordering as an enum
.type Ordering <: symbol
.decl ordering(o:Ordering)

.decl unordered_ordering(o:Ordering)
.decl monotonic_ordering(o:Ordering)
.decl acquire_ordering(o:Ordering)
.decl release_ordering(o:Ordering)
.decl acq_rel_ordering(o:Ordering)
.decl seq_cst_ordering(o:Ordering)
...
.output unification_subobjects.alloc_subregion_at_any_array_index (compress=true)
.output unification_subobjects.alloc_subregion_at_array_index (compress=true)
//--End of  ./debug.project
//
//  included files list
//
/*
#include <./debug.project> // 1
#include <./subset-and-unification.project> // 2
#include <./common.project> // 3
#include <./schema/schema.project> // 4
#include <./schema/debug.dl> // 5
#include <./schema/calling-convention.dl> // 6
#include <./schema/ordering.dl> // 7
#include <./schema/type.dl> // 8
#include <./schema/operand.dl> // 9
#include <./schema/asm.dl> // 10
#include <./schema/global.dl> // 11
#include <./schema/func.dl> // 12
#include <./schema/constants.dl> // 13
#include <./schema/instr.dl> // 14
#include <./schema/basic-block.dl> // 15
#include <./schema/add-instr.dl> // 16
#include <./schema/sub-instr.dl> // 17
#include <./schema/mul-instr.dl> // 18
#include <./schema/sdiv-instr.dl> // 19
#include <./schema/srem-instr.dl> // 20
#include <./schema/udiv-instr.dl> // 21
#include <./schema/urem-instr.dl> // 22
#include <./schema/fadd-instr.dl> // 23
#include <./schema/fsub-instr.dl> // 24
#include <./schema/fmul-instr.dl> // 25
#include <./schema/fdiv-instr.dl> // 26
#include <./schema/frem-instr.dl> // 27
#include <./schema/and-instr.dl> // 28
#include <./schema/or-instr.dl> // 29
#include <./schema/xor-instr.dl> // 30
#include <./schema/ashr-instr.dl> // 31
#include <./schema/lshr-instr.dl> // 32
#include <./schema/shl-instr.dl> // 33
#include <./schema/icmp-instr.dl> // 34
#include <./schema/fcmp-instr.dl> // 35
#include <./schema/bitcast-instr.dl> // 36
#include <./schema/inttoptr-instr.dl> // 37
#include <./schema/ptrtoint-instr.dl> // 38
#include <./schema/fpext-instr.dl> // 39
#include <./schema/sext-instr.dl> // 40
#include <./schema/zext-instr.dl> // 41
#include <./schema/fptosi-instr.dl> // 42
#include <./schema/fptoui-instr.dl> // 43
#include <./schema/sitofp-instr.dl> // 44
#include <./schema/uitofp-instr.dl> // 45
#include <./schema/trunc-instr.dl> // 46
#include <./schema/fptrunc-instr.dl> // 47
#include <./schema/br-instr.dl> // 48
#include <./schema/indirectbr-instr.dl> // 49
#include <./schema/phi-instr.dl> // 50
#include <./schema/switch-instr.dl> // 51
#include <./schema/select-instr.dl> // 52
#include <./schema/alloca-instr.dl> // 53
#include <./schema/load-instr.dl> // 54
#include <./schema/store-instr.dl> // 55
#include <./schema/atomicrmw-instr.dl> // 56
#include <./schema/cmpxchg-instr.dl> // 57
#include <./schema/ret-instr.dl> // 58
#include <./schema/call-instr.dl> // 59
#include <./schema/invoke-instr.dl> // 60
#include <./schema/fence-instr.dl> // 61
#include <./schema/landingpad-instr.dl> // 62
#include <./schema/resume-instr.dl> // 63
#include <./schema/extractelement-instr.dl> // 64
#include <./schema/insertelement-instr.dl> // 65
#include <./schema/shufflevector-instr.dl> // 66
#include <./schema/getelementptr-instr.dl> // 67
#include <./schema/extractvalue-instr.dl> // 68
#include <./schema/insertvalue-instr.dl> // 69
#include <./schema/unreachable-instr.dl> // 70
#include <./schema/va-arg-instr.dl> // 71
#include <./schema/activate-sanity.dl> // 72
#include <./import/import.project> // 73
#include <./import/import.dl> // 74
#include <./import/../../FactGenerator/include/predicates.inc> // 75
#include <./symbol-lookup/symbol-lookup.project> // 76
#include <./symbol-lookup/resolve-func-calls.dl> // 77
#include <./callgraph/callgraph.project> // 78
#include <./callgraph/entry-points.dl> // 79
#include <./points-to/points-to.project> // 80
#include <./points-to/argv.dl> // 81
#include <./points-to/allocations-decl.dl> // 82
#include <./points-to/allocations.dl> // 83
#include <./points-to/allocations-globals.dl> // 84
#include <./points-to/allocations-sizes.dl> // 85
#include <./points-to/allocations-type.dl> // 86
#include <./points-to/allocations-subobjects.dl> // 87
#include <./points-to/assignment.dl> // 88
#include <./points-to/at-exit.dl> // 89
#include <./points-to/type-compatibility.dl> // 90
#include <./points-to/points-to-options.dl> // 91
#include <./points-to/class-type.dl> // 92
#include <./points-to/virtual-tables.dl> // 93
#include <./points-to/type-back-propagation.dl> // 94
#include <./points-to/constant-init.dl> // 95
#include <./points-to/constant-exprs.dl> // 96
#include <./points-to/constant-points-to.dl> // 97
#include <./points-to/allocations-subobjects-aliases.dl> // 98
#include <./points-to/core.dl> // 99
#include <./points-to/cplusplus.dl> // 100
#include <./points-to/strip-context-projections.dl> // 101
#include <./points-to/interprocedural.dl> // 102
#include <./points-to/memcpy.dl> // 103
#include <./points-to/field-sensitivity.dl> // 104
#include <./points-to/cplusplus-exceptions.dl> // 105
#include <./points-to/signatures.dl> // 106
#include <./points-to/types.dl> // 107
#include <./points-to/region.dl> // 108
#include <./context/context.project> // 109
#include <./context/drop.dl> // 110
#include <./context/interface.dl> // 111
#include <./context/lift.dl> // 112
#include <./options/user-options.dl> // 113
#include <./export/subset.dl> // 114
#include <./export/unification.dl> // 115
#include <./points-to/assertions.dl> // 116
#include <./points-to/points-to-statistics.dl> // 117
#include <./points-to/subset.dl> // 118
#include <./points-to/unification.dl> // 119
#include <./export/statistics.dl> // 120
#include <./export/debug-output.dl> // 121
#include <./points-to/debug.dl> // 122
*/
mingodad commented 2 years ago

Also see this discussion https://github.com/souffle-lang/souffle/discussions/2350 about the documentation comments (near the end right now).

mingodad commented 2 years ago

It seems that this project datalog part can be simplified to this:

#include "common.project"

.comp CcLyzerSubset {
    #include "export/subset.dl"
    #include "points-to/subset.dl"
}

.comp CcLyzerUnification {
    #include "export/unification.dl"
    #include "points-to/unification.dl"
}

.comp CcLyserDebug : CcLyzerSubset, CcLyzerUnification {
    #include "points-to/assertions.dl"
    #include "points-to/points-to-statistics.dl"
    #include "export/statistics.dl"
    #include "export/debug-output.dl"
    #include "points-to/debug.dl"

    // These are relations from components that aren't detected using
    // generate-debug-output.sh.

    .output subset_aliases.alloc_aliases (compress=true)
    .output subset_aliases.alloc_matches (compress=true)
    .output subset_allocations.alloc_with_ctx (compress=true)
    .output subset_allocation_type.allocation_type (compress=true)
    .output subset_subobjects._alloc_subregion (compress=true)
    .output subset_subobjects.alloc_subregion_at_array_index (compress=true)
    .output subset_subobjects.alloc_subregion_at_field (compress=true)
    .output subset_subobjects.alloc_subregion_at_path (compress=true)
    .output subset_subobjects.alloc_subregion_offset (compress=true)
    .output subset_lift._allocation_with_context (compress=true)
    .output subset_memcpy.rec_memcpy (compress=true)
    .output subset_memcpy._try_memcpy (compress=true)
    .output subset_memcpy._stripctx_memcpy (compress=true)
    .output subset_memcpy._type_compatible_memcpy (compress=true)
    .output subset_memcpy._well_typed_and_sized_memcpy (compress=true)
    .output subset_memcpy._do_memcpy (compress=true)
    .output subset.callgraph.callgraph_edge (compress=true)
    .output subset._merge.merge (compress=true)
    .output subset._merge.assert_reachable_calls_have_contexts (compress=true)
    .output subset._merge.assert_reachable_calls_have_context_items (compress=true)
    .output subset_gep.gep_indexes_from (compress=true)
    .output subset_gep.gep_points_to (compress=true)
    .output subset_gep._gep_type_compatible (compress=true)
    .output subset_gep._gep_last_index_points_to (compress=true)
    .output subset.type_indication.assign_rebase_alloc (compress=true)
    .output subset.type_indication.heap_allocation_by_type_instr (compress=true)
    .output subset.type_indication.ty_indication (compress=true)
    .output subset.type_indication.ty_indication1 (compress=true)
    .output subset.type_indication.ty_indication2 (compress=true)
    .output subset.type_indication.ty_indication3 (compress=true)

    .output unification_aliases.alloc_aliases (compress=true)
    .output unification_aliases.alloc_matches (compress=true)
    .output unification_allocation_type.allocation_type (compress=true)
    .output unification_subobjects._alloc_subregion (compress=true)
    .output unification_subobjects.alloc_subregion_at_array_index (compress=true)
    .output unification_subobjects.alloc_subregion_at_field (compress=true)
    .output unification_subobjects.alloc_subregion_at_path (compress=true)
    .output unification_subobjects.alloc_subregion_offset (compress=true)
    .output unification_memcpy.rec_memcpy (compress=true)
    .output unification_memcpy._try_memcpy (compress=true)
    .output unification_memcpy._stripctx_memcpy (compress=true)
    .output unification_memcpy._type_compatible_memcpy (compress=true)
    .output unification_memcpy._well_typed_and_sized_memcpy (compress=true)
    .output unification_memcpy._do_memcpy (compress=true)
    .output unification.callgraph.callgraph_edge (compress=true)
    .output unification._merge.merge (compress=true)
    .output unification._merge.assert_reachable_calls_have_contexts (compress=true)
    .output unification._merge.assert_reachable_calls_have_context_items (compress=true)
    .output unification.type_indication.assign_rebase_alloc (compress=true)
    .output unification.type_indication.heap_allocation_by_type_instr (compress=true)
    .output unification.type_indication.ty_indication (compress=true)
    .output unification.type_indication.ty_indication1 (compress=true)
    .output unification.type_indication.ty_indication2 (compress=true)
    .output unification.type_indication.ty_indication3 (compress=true)

    .output unification.operand_points_to (compress=true)
    .output unification.ptr_points_to (compress=true)
    .output unification._gep_alloc_info (compress=true)
    .output unification.unify (compress=true)
    .output unification.unify_ptr (compress=true)
    .output unification.unify_var (compress=true)
    .output unification.unify_ptr_expanded (compress=true)
    .output unification.unify_var_expanded (compress=true)
    .output unification.unify_repr (compress=true)
    .output unification.var_points_to (compress=true)
    .output unification.var_points_to_final (compress=true)
    .output unification_allocations.alloc_with_ctx (compress=true)
    .output unification_gep.gep_indexes_from (compress=true)
    .output unification_gep.gep_points_to (compress=true)
    .output unification_gep._gep_type_compatible (compress=true)
    .output unification_gep._gep_last_index_points_to (compress=true)
    .output unification_subobjects._alloc_subregion (compress=true)
    .output unification_subobjects.alloc_subregion_at_path (compress=true)
    .output unification_subobjects.alloc_subregion_at_field (compress=true)
    .output unification_subobjects.alloc_subregion_at_any_array_index (compress=true)
    .output unification_subobjects.alloc_subregion_at_array_index (compress=true)
}