Help needed to run psychec

jordiae commented 3 years ago

Hi, thanks for your contribution. This project is very interesting.

I'm trying to run pyschec and I've found 2 issues:

Even after running cmake and make as advised in the README, the psychecgen binary is not generated.
Executing the cnip binary doesn't produce any output/file, except when I ask it to dump the AST. For instance, the command: ./cnip --file node.c --C-infer has no effect at all.

What am I doing wrong? Many thanks in advance.

aytey commented 3 years ago

psychecgen only exists in the original branch. If you need psychecgen, you need to build that branch.

The current master just does parsing and AST dumping, but doesn't do the program completion like the original branch does.

aytey commented 3 years ago

I should say, depending on what machine you use, the version of GHC in the Stack configuration file might not allow you to build psychecgen.

I think the issue was that Stack tried to pull in a version of GHC that was too old to build on a recent Linux distro. My fork of psychec uses lts-7.1 over lts-5.1 (because 5.1 is too old).

jordiae commented 3 years ago

I should say, depending on what machine you use, the version of GHC in the Stack configuration file might not allow you to build psychecgen.

I think the issue was that Stack tried to pull in a version of GHC that was too old to build on a recent Linux distro. My fork of psychec uses lts-7.1 over lts-5.1 (because 5.1 is too old).

Thanks for your answer! I can psychecgen now, but when trying to run cnip now I get this error:

jordiae@jordiaebook:~/Downloads/psychec$ ./cnip.sh -f gcc -c node.c
cnippet: fatal: exception invoking process: psychecsolver-exe
Traceback (most recent call last): think I can build it, 
  File "/home/jordiae/Downloads/psychec/cnippet/Process.py", line 27, in execute
    code = subprocess.call(cmd, *args, **kwargs)
  File "/usr/lib/python3.8/subprocess.py", line 340, in call
    with Popen(*popenargs, **kwargs) as p:
  File "/usr/lib/python3.8/subprocess.py", line 858, in __init__
    self._execute_child(args, executable, preexec_fn, close_fds,
  File "/usr/lib/python3.8/subprocess.py", line 1704, in _execute_child
    raise child_exception_type(errno_num, err_msg, err_filename)
FileNotFoundError: [Errno 2] No such file or directory: 'psychecsolver-exe'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/jordiae/Downloads/psychec/cnippet/Process.py", line 29, in execute
    sys.exit(
SystemExit: 4

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "./cnippet/Main.py", line 125, in <module>
    code = driver.execute()
  File "/home/jordiae/Downloads/psychec/cnippet/Driver.py", line 112, in execute
    self._compile_unit(unit, cc_cmd)
  File "/home/jordiae/Downloads/psychec/cnippet/Driver.py", line 66, in _compile_unit
    self.psyche.solve_constraints(unit)
  File "/home/jordiae/Downloads/psychec/cnippet/PsycheCFacade.py", line 93, in solve_constraints
    ok = execute(PsycheCFacade.ID(), cmd)
  File "/home/jordiae/Downloads/psychec/cnippet/Process.py", line 32, in execute
    h.report(code)
UnboundLocalError: local variable 'code' referenced before assignment

My goal is to get the same output as you got with Anghabench.

aytey commented 3 years ago

Is the path to psychecsolver-exe (which might be one level above the CMake build folder) on $PATH?

jordiae commented 3 years ago

Is the path to psychecsolver-exe (which might be one level above the CMake build folder) on $PATH?

It is not. But it's not in the directory, either:

jordiae@jordiaebook:~/Downloads/psychec$ find . -name "*psychec*"
./C/CMakeFiles/psychecfe.dir
./C/stdlib-support/CMakeFiles/psychecstd.dir
./CMakeFiles/psychecgen.dir
./libpsychecstd.so
./psychecgen
./frontend/CMakeFiles/psychecfe.dir
./frontend/libpsychecfe.so
./solver/psychecsolver.cabal
./stdlib-support/CMakeFiles/psychecstd.dir
./common/CMakeFiles/psychecommon.dir

aytey commented 3 years ago

Oh, did you build in the "main" directory? That's sort of bad practise.

On a completely fresh clone, try this:

cd psychec
mkdir build
cd build
cmake ..

you don't actually have to do the "make" because calling cmake will build psychecsolver-exe in the directory above:

-- Solver build: 0  Building all executables for `psychecsolver' once. After a successful build of all of them, only specified executables will be rebuilt.
psychecsolver> configure (lib + exe)
Configuring psychecsolver-0.1.0...
Warning: 'license-file: ../LICENSE' is a relative path outside of the source
...skipping...
[ 8 of 26] Compiling Data.StdDef      ( src/Data/StdDef.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/StdDef.o )
[ 9 of 26] Compiling Data.StdInt      ( src/Data/StdInt.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/StdInt.o )
[10 of 26] Compiling Data.IntTypes    ( src/Data/IntTypes.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/IntTypes.o )
[11 of 26] Compiling Data.WChar       ( src/Data/WChar.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/WChar.o )
[12 of 26] Compiling Data.StdLib      ( src/Data/StdLib.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/StdLib.o )
[13 of 26] Compiling Data.StdIO       ( src/Data/StdIO.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/StdIO.o )
[14 of 26] Compiling Data.Math        ( src/Data/Math.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/Math.o )
[15 of 26] Compiling Data.WCType      ( src/Data/WCType.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/WCType.o )
[16 of 26] Compiling Solver.ConversionRules ( src/Solver/ConversionRules.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/ConversionRules.o )
[17 of 26] Compiling Solver.SolverMonad ( src/Solver/SolverMonad.lhs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/SolverMonad.o )
[18 of 26] Compiling Solver.Decaying  ( src/Solver/Decaying.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/Decaying.o )
[19 of 26] Compiling Solver.Retypeable ( src/Solver/Retypeable.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/Retypeable.o )
[20 of 26] Compiling Solver.Unification ( src/Solver/Unification.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/Unification.o )
[21 of 26] Compiling Parser.ConstraintParser ( src/Parser/ConstraintParser.lhs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Parser/ConstraintParser.o )
[22 of 26] Compiling Utils.DeclSorter ( src/Utils/DeclSorter.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Utils/DeclSorter.o )
[23 of 26] Compiling Data.String      ( src/Data/String.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/String.o )
[24 of 26] Compiling Solver.ContextAssemble ( src/Solver/ContextAssemble.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/ContextAssemble.o )
[25 of 26] Compiling Solver.ConstraintSolver ( src/Solver/ConstraintSolver.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/ConstraintSolver.o )
[26 of 26] Compiling Utils.Writer     ( src/Utils/Writer.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Utils/Writer.o )
Preprocessing executable 'psychecsolver-exe' for psychecsolver-0.1.0...
[1 of 1] Compiling Main             ( app/Main.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/psychecsolver-exe/psychecsolver-exe-tmp/Main.o )
Linking .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/psychecsolver-exe/psychecsolver-exe ...
psychecsolver> copy/register
Installing library in
/home/avj/clones/psychec/original/solver/.stack-work/install/x86_64-linux-tinfo6/6858c497b6b5db9ea9db1e9026374b9c7b092e1e36f1b2a66fb28811777ec8ca/8.0.1/lib/x86_64-linux-ghc-8.0.1/psychecsolver-0.1.0-85KW72IvrpJFv8P1d2UTBK
Installing executable(s) in
/home/avj/clones/psychec/original/solver/.stack-work/install/x86_64-linux-tinfo6/6858c497b6b5db9ea9db1e9026374b9c7b092e1e36f1b2a66fb28811777ec8ca/8.0.1/bin
Registering psychecsolver-0.1.0...
Copying from /home/avj/clones/psychec/original/solver/.stack-work/install/x86_64-linux-tinfo6/6858c497b6b5db9ea9db1e9026374b9c7b092e1e36f1b2a66fb28811777ec8ca/8.0.1/bin/psychecsolver-exe to /home/avj/clones/psychec/original/psychecsolver-exe

Copied executables to /home/avj/clones/psychec/original:
- psychecsolver-exe

Warning: Installation path /home/avj/clones/psychec/original
         not found on the PATH environment variable.
-- Configuring done
-- Generating done
-- Build files have been written to: /home/avj/clones/psychec/original/build

So you should now find psychecsolver-exe in the parent directory.

jordiae commented 3 years ago

Oh, did you build in the "main" directory? That's sort of bad practise.

On a completely fresh clone, try this:

cd psychec
mkdir build
cd build
cmake ..

you don't actually have to do the "make" because calling cmake will build psychecsolver-exe in the directory above:

-- Solver build: 0  Building all executables for `psychecsolver' once. After a successful build of all of them, only specified executables will be rebuilt.
psychecsolver> configure (lib + exe)
Configuring psychecsolver-0.1.0...
Warning: 'license-file: ../LICENSE' is a relative path outside of the source
...skipping...
[ 8 of 26] Compiling Data.StdDef      ( src/Data/StdDef.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/StdDef.o )
[ 9 of 26] Compiling Data.StdInt      ( src/Data/StdInt.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/StdInt.o )
[10 of 26] Compiling Data.IntTypes    ( src/Data/IntTypes.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/IntTypes.o )
[11 of 26] Compiling Data.WChar       ( src/Data/WChar.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/WChar.o )
[12 of 26] Compiling Data.StdLib      ( src/Data/StdLib.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/StdLib.o )
[13 of 26] Compiling Data.StdIO       ( src/Data/StdIO.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/StdIO.o )
[14 of 26] Compiling Data.Math        ( src/Data/Math.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/Math.o )
[15 of 26] Compiling Data.WCType      ( src/Data/WCType.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/WCType.o )
[16 of 26] Compiling Solver.ConversionRules ( src/Solver/ConversionRules.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/ConversionRules.o )
[17 of 26] Compiling Solver.SolverMonad ( src/Solver/SolverMonad.lhs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/SolverMonad.o )
[18 of 26] Compiling Solver.Decaying  ( src/Solver/Decaying.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/Decaying.o )
[19 of 26] Compiling Solver.Retypeable ( src/Solver/Retypeable.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/Retypeable.o )
[20 of 26] Compiling Solver.Unification ( src/Solver/Unification.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/Unification.o )
[21 of 26] Compiling Parser.ConstraintParser ( src/Parser/ConstraintParser.lhs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Parser/ConstraintParser.o )
[22 of 26] Compiling Utils.DeclSorter ( src/Utils/DeclSorter.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Utils/DeclSorter.o )
[23 of 26] Compiling Data.String      ( src/Data/String.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Data/String.o )
[24 of 26] Compiling Solver.ContextAssemble ( src/Solver/ContextAssemble.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/ContextAssemble.o )
[25 of 26] Compiling Solver.ConstraintSolver ( src/Solver/ConstraintSolver.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Solver/ConstraintSolver.o )
[26 of 26] Compiling Utils.Writer     ( src/Utils/Writer.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/Utils/Writer.o )
Preprocessing executable 'psychecsolver-exe' for psychecsolver-0.1.0...
[1 of 1] Compiling Main             ( app/Main.hs, .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/psychecsolver-exe/psychecsolver-exe-tmp/Main.o )
Linking .stack-work/dist/x86_64-linux-tinfo6/Cabal-1.24.0.0/build/psychecsolver-exe/psychecsolver-exe ...
psychecsolver> copy/register
Installing library in
/home/avj/clones/psychec/original/solver/.stack-work/install/x86_64-linux-tinfo6/6858c497b6b5db9ea9db1e9026374b9c7b092e1e36f1b2a66fb28811777ec8ca/8.0.1/lib/x86_64-linux-ghc-8.0.1/psychecsolver-0.1.0-85KW72IvrpJFv8P1d2UTBK
Installing executable(s) in
/home/avj/clones/psychec/original/solver/.stack-work/install/x86_64-linux-tinfo6/6858c497b6b5db9ea9db1e9026374b9c7b092e1e36f1b2a66fb28811777ec8ca/8.0.1/bin
Registering psychecsolver-0.1.0...
Copying from /home/avj/clones/psychec/original/solver/.stack-work/install/x86_64-linux-tinfo6/6858c497b6b5db9ea9db1e9026374b9c7b092e1e36f1b2a66fb28811777ec8ca/8.0.1/bin/psychecsolver-exe to /home/avj/clones/psychec/original/psychecsolver-exe

Copied executables to /home/avj/clones/psychec/original:
- psychecsolver-exe

Warning: Installation path /home/avj/clones/psychec/original
         not found on the PATH environment variable.
-- Configuring done
-- Generating done
-- Build files have been written to: /home/avj/clones/psychec/original/build

So you should now find psychecsolver-exe in the parent directory.

Yes, thanks for your answer. However:

jordiae@jordiaebook:~/Downloads/psychec/build$ cmake ..
-- The C compiler identification is GNU 9.3.0
-- The CXX compiler identification is GNU 9.3.0
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Solver build: No such file or directory  
-- Configuring done
-- Generating done
-- Build files have been written to: /home/jordiae/Downloads/psychec/build

Notice -- Solver build: No such file or directory . Indeed, it's not generated.

aytey commented 3 years ago

Which branch are you on?

jordiae commented 3 years ago

Which branch are you on?

git checkout original

aytey commented 3 years ago

Hmm, then you should have https://github.com/ltcmelo/psychec/tree/original/solver

jordiae commented 3 years ago

Hmm, then you should have https://github.com/ltcmelo/psychec/tree/original/solver

I have it! But I still get Solver build: No such file or directory. I also have GHC and Cabal installed...

aytey commented 3 years ago

And Stack? You shouldn’t need to install GHC yourself as Stack will install the right version for you.

Try:

cd solver
stack build

jordiae commented 3 years ago

And Stack? You shouldn’t need to install GHC yourself as Stack will install the right version for you.

Try:
cd solver
stack build

I didn't! Gonna try that now, thanks!

jordiae commented 3 years ago

It works, many thanks for your help @andrewvaughanj

ltcmelo commented 3 years ago

@andrewvaughanj , many thanks for the support to @jordiae :-)

ltcmelo / psychec

Help needed to run psychec #48