Skip to content

Commit

Permalink
adding start to rules
Browse files Browse the repository at this point in the history
Signed-off-by: vsoch <vsoch@users.noreply.github.com>
  • Loading branch information
vsoch committed Mar 23, 2021
1 parent 5984ed6 commit 0c8e3d8
Show file tree
Hide file tree
Showing 4 changed files with 471 additions and 22 deletions.
21 changes: 21 additions & 0 deletions abi-python/python/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -115,3 +115,24 @@ we can use that to try and write a logic program. I also added in the third libr
because it became clear that we could never know the set of symbols that are supposed
to be provided, and these are the `needed_symbol` groups. Now I'm working on writing logic in [is_compatible.lp](is_compatible.lp)
to first derive this set of needed symbols. After that, I'll look at [compute_diff](https://github.com/woodard/libabigail/blob/40aab37cf04214504804ae9fe7b6c7ff4fd1500f/src/abg-comparison.cc#L11031) in libabigail to derive more rules after that.

See [rules.md](rules.md) for breaking down this function in libabigail. In the facts,
I'm currently at having a check over symbols and for just one architecture. It's pretty
limited but it's a start!

```bash
(clingo-env) root@b32e9108f711:/code/python# clingo facts.lp is_compatible.lp
clingo version 5.4.0
Reading from facts.lp ...
Solving...
Answer: 1
architecture_count(1) total_missing(4)
SATISFIABLE

Models : 1
Calls : 1
Time : 0.006s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.006s
```
Note that since we don't take unique orders of things, the missing is likely doubled.
But for now we don't care because it's > 0.
4 changes: 4 additions & 0 deletions abi-python/python/asp.py
Original file line number Diff line number Diff line change
Expand Up @@ -587,6 +587,10 @@ def generate_corpus_metadata(self, corpora):
# Note that we could update these to just be corpus_attr, but I'm
# starting with testing a more detailed approach for now.

# If the corpus has a soname:
if corpus.soname:
self.gen.fact(fn.corpus_soname(corpus.path, corpus.soname))

# File class (also at elffile.elfclass or corpus.elfclass
self.gen.fact(fn.corpus_elf_class(corpus.path, hdr["e_ident"]["EI_CLASS"]))

Expand Down
58 changes: 36 additions & 22 deletions abi-python/python/is_compatible.lp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,16 @@
% corpus("/code/simple-example/cpp/libmath-v1.so").
% We can maybe use a basename
% corpus_basename("/code/simple-example/cpp/libmath-v1.so","libmath-v1.so").
% If we are deriving from spack, I also don't see why we can't include
% other libraries (we are sure about) that are needed to find extra symbols,
% although libabigail doesn't do that.

%=============================================================================
% Matching function and variable symbols
% symbols are missing if they are needed (present in the working library),
% not undefined in the working library (indicating they come from elsewhere)
% and undefined in both the potential library and binary.
%=============================================================================

% A symbol is undefined in this case.
symbol_is_undefined(Corpus, Symbol) :- symbol_definition(Corpus, Symbol, "UND").
Expand Down Expand Up @@ -48,37 +58,41 @@ missing_symbols(CorpusA, CorpusB, Symbol)
:- symbol_is_needed(Symbol),
both_symbols_undefined(CorpusA, CorpusB, Symbol).

% Two corpora have a compatible symbol if it's shared, and at least one is defined
% This is my attempt to capture an OR
%compatible_symbols(CorpusA, CorpusB, Symbol)
% :- shared_symbol(CorpusA, CorpusB, Symbol),
% symbol_is_undefined(CorpusA, Symbol).

%compatible_symbols(CorpusA, CorpusB, Symbol)
% :- shared_symbol(CorpusA, CorpusB, Symbol),
% symbol_is_undefined(CorpusB, Symbol).

% a missing symbol is not defined in either (indicating we are missing libs)
%missing_symbols(CorpusA, CorpusB, Symbol)
% :- shared_symbol(CorpusA, CorpusB, Symbol),
% both_symbols_undefined(CorpusA, CorpusB, Symbol).

% Try to create a count of missing symbols
% TODO: this will be double if we count CorpusA, CorpusB and CorpusB, CorpusA (twice)
get_missing_symbols(S) :- missing_symbols(_, _, S).
total_missing(N) :- #count{X:get_missing_symbols(X)} = K, K=N.

%total_compatible(N) :- #count{X:get_compatible_symbols(X)} = K, K=N.


%=============================================================================
% Matching soname and architecture
% libraries must have matching soname and architecture
%=============================================================================

% libabigail just compares the libs, but why not compare to the binary too?
%shared_architecture(CorpusA, CorpusB)
% :- corpus_elf_machine(CorpusA, _, A)
get_architecture(A) :- corpus_elf_machine(_, A).
architecture_count(N) :- #count{X:get_architecture(X)} = K, K=N.

% todo: I don't think my data has sonames, need to add or figure out why not in
% dynamic tags
% get_soname(A) :- corpus_elf_soname(_, A).
% soname_count(N) :- #count{X:get_soname(X)} = K, K=N.

% TODO I will want to print this out more clearly, probably the is_compatible
% function could use arguments for Corpora.
% Two corpora are compatible if:
are_compatible()

% there are no missing symbols
:- total_missing(N) = 0.
:- total_missing(N) == 0.

% TODO I will want to print this out more clearly, probably the is_compatible
% function could use arguments for Corpora.
%#show compatible_symbols/3.
%#show total_shared/1.
%#show total_compatible/1.
#show missing_symbols/3.
% there is only one architecture
:- architecture_count(N) == 1.

#show total_missing/1.
#show architecture_count/1.
%#show soname_count/1.

0 comments on commit 0c8e3d8

Please sign in to comment.