[ldv-project] Queries in running the LDV.
Ilja Zakharov
ilja.zakharov at ispras.ru
Tue Jul 2 16:10:29 MSK 2019
You can put there the "**" expression that means to check all available
modules. As you compiled only your own module this should work.
вт, 2 июл. 2019 г. в 16:00, Puneet Gupta <PUNEETG at xilinx.com>:
> If I have to only check my external kernel module , what I have to give in
> the “add targets”?
>
> Is it the name of the .ko module?
>
>
>
> {
>
> "Class": "Verification of Linux kernel modules",
>
> "build base": "clade",
>
> "program": "Linux",
>
> "version": "3.14",
>
> "fragmentation set": "Modules",
>
> "add targets": [
>
> "drivers/ata/pata_arasan_cf.ko",
>
> "drivers/idle/i7300_idle.ko",
>
> "drivers/uwb/hwa-rc.ko"
>
> ],
>
> "specifications set": "Linux 3.14 (base)",
>
> "requirements": [
>
> "linux:arch:io",
>
> "linux:drivers:clk1",
>
> "linux:kernel:locking:mutex",
>
> "linux:memory safety"
>
> ]
>
> }
>
>
>
> *From:* Puneet Gupta
> *Sent:* Tuesday, July 2, 2019 6:14 PM
> *To:* Ilja Zakharov <ilja.zakharov at ispras.ru>
> *Cc:* Alexey Khoroshilov <khoroshilov at ispras.ru>;
> ldv-project at linuxtesting.org
> *Subject:* RE: [ldv-project] Queries in running the LDV.
>
>
>
> Hi Ilja,
>
>
>
> At step 3 , I was able to open the localhost:8998 , and login as
> manager:manager. Then I entered to my kernel module directory and ran
> “clade-intercept make” and executed the step5.
>
> In web interface also , I have edited the job.json file as you mentioned.
> But still I am not able to see the static analysis report in the webpage.
>
>
>
> Can you please tell me how to view the report. If you can send an example
> , that would be helpful too.
>
>
>
> Thanks,
>
> Puneet
>
>
>
> *From:* Ilja Zakharov <ilja.zakharov at ispras.ru>
> *Sent:* Friday, June 28, 2019 2:02 PM
> *To:* Puneet Gupta <PUNEETG at xilinx.com>
> *Cc:* Alexey Khoroshilov <khoroshilov at ispras.ru>;
> ldv-project at linuxtesting.org
> *Subject:* Re: [ldv-project] Queries in running the LDV.
>
>
>
> EXTERNAL EMAIL
>
> Hi Puneet,
>
> Thanks for your interest in the Klever verification framework.
>
> To verify your separate driver you should do the following steps:
> 1) First, be sure that you have some kernel version sources files to
> compile your driver with. It is better to choose versions of Linux in
> between 3.14 and 4.6.7. It is possible to check a driver with a newer
> version of the Linux kernel but it will require additional steps. Both the
> driver and Kernel should be configured and compiled for x86_64 architecture
> preferably.
>
> 2) Install the Klever framework according to this manual:
> https://klever.readthedocs.io/en/latest/deploy.html
> (!) Klever will need a lot of computational resources to run, so avoid
> installing it on a laptop. If your driver is an open source we can even
> give you access to a virtual machine with Klever to try it.
>
> 3) Before trying to verify your own driver just ensure that all is
> installed correctly. To do that open localhost:8998, log in as
> manager:manager and try to solve a preexisting verification job there. If
> all goes smoothly, go to the next step.
>
> 4) Prepare a build base for your driver. To do that just configure the
> kernel and your driver and build it with a prefix command:
>
> clade-intercept <your compilation command>"
>
> (An example: clade-intercept make -j8 M=drivers/net/usb)
> Prepare the environment:
> export PATH=$KLEVER_DEPLOY_DIR/klever-addons/CIF/bin/:$PATH
> Where $KLEVER_DEPLOY_DIR is an absolute path to Klever installation
> directory. Run "cif --help" to be sure that path is correct.
> Then run the second command to create the build base:
> clade-all -p linux_kernel cmds.txt
>
> After the command, you will have a directory named "clade". I refer to it
> as <clade dir> in the next steps below.
>
> 5. After Klever installation, you can build the kernel and create a build
> base.
> a) Modify the configuration file that you have used for Klever
> installation and add there the following entry: "Klever Build Bases":
> ["<clade dir>"]
> b) Run again installation command exactly as at installation but replace
> keyword "install" with "update"
>
> 6) That is almost all. Go to the web interface. Copy your test job, click
> "modify", choose job.json file and in the opened editor window set proper
> setting and identifiers of rules to check. You will need there to set
> fields "build base" as "clade", "requirements" as ["linux:memory safety"]
> (or add additional rules to check).
>
> If you need an example write me back.
>
> 7) To uninstall Klever use installation command with command "uninstall"
> instead of "install".
>
>
> Please, do not hesitate to write me back and ask questions.
>
> Best,
> Ilia Zakharov
>
>
>
> чт, 27 июн. 2019 г. в 20:57, Puneet Gupta <PUNEETG at xilinx.com>:
>
> Hi Alexey,
>
>
>
> Thanks for your mail.
>
>
>
> I have downloaded the klever package and managed to install it also by
> following the instructions given in the “local deployment” section.
>
> https://buildmedia.readthedocs.org/media/pdf/klever/latest/klever.pdf
>
>
>
> Can you guide me how to run the klever tool on my kernel module? Is there
> any doc which I can follow in which step by step the instructions are given?
>
>
>
> Currently I have my kernel module as a tar.bz2 and I want to do static
> analysis on it.
>
>
>
> I tried running ,
>
> - cd bridge
> - python3 manage.py test
>
>
>
> I got the following error:
>
> * File "<frozen importlib._bootstrap>", line 219, in
> _call_with_frames_removed*
>
> * File
> "/group/cdc_hd/members/puneetg/kernel_static_analysis/klever/klever-inst/klever/bridge/bridge/__init__.py",
> line 21, in <module>*
>
> * from bridge.settings import DATABASES*
>
> *ModuleNotFoundError: No module named 'bridge.settings'*
>
>
>
> I can also see “linux-3.14.79.tar.xz” tar file in “build bases” directory.
> Shall I need to place my external module tar file in that directory and run
> some tests?
>
>
>
> Thanks,
>
> Puneet
>
>
>
>
>
> *From:* Alexey Khoroshilov <khoroshilov at ispras.ru>
> *Sent:* Friday, June 21, 2019 9:16 PM
> *To:* Puneet Gupta <PUNEETG at xilinx.com>; ldv-project at linuxtesting.org
> *Subject:* Re: Queries in running the LDV.
>
>
>
> EXTERNAL EMAIL
>
> Dear Puneet,
>
> It seems you use LDV Tools, but it was superseded by our newer KLEVER
> Framework [1,2].
> So, we suggest to use the newer tool.
>
> As for memory leak rule, we had a prototype of such rule in LDV Tools (104
> [3]), but it was not maintained and it is not available in KLEVER. So, we
> suggest to check code against some memory safety rules ((KLEVER rule id:
> "linux:memory safety", please note that string operations are not supported
> yet) or some Linux specific rules like mutex lock [4] or
> clock_enable/clock_disable [5].
>
> [1] http://linuxtesting.org/04-07-2018
> [2] https://forge.ispras.ru/projects/klever
> [3] https://forge.ispras.ru/issues/2735
> [4] https://forge.ispras.ru/issues/1940 (KLEVER rule ids:
> "linux:kernel:locking:mutex")
> [5] https://forge.ispras.ru/issues/8785 (KLEVER rule ids:
> "linux:drivers:clk1", "linux:drivers:clk2")
>
> Best regards,
> Alexey Khoroshilov
> Linux Verification Center, ISPRAS
>
>
> On 21.06.2019 8:30, Puneet Gupta wrote:
>
> Hi,
>
>
>
> I am using LDV for running static analysis for my external driver.
>
>
>
> I have few questions :
>
> - The driver has many files to be compiled, but it seems the LDV is
> only reporting out the errors for the file which is mentioned in ‘obj-m’.
> How can I get result for all the files?
> - What is meant by the error: “attempting to take field offset lock of
> expression priv at stop whose value is Top”. I am getting only these
> errors for my file.
> - To test the LDV , I did kmalloc and didn’t freed the memory
> returned. But the output on the webpage is not showing an error for that
> memory leak. Have I need to pass some separate rule for detecting the
> memory leaks?
>
>
>
> I am using 32_7a rule for running the driver, as given in the example in
> the LDV standard doc.
>
>
>
> Thanks,
>
> Puneet
>
> This email and any attachments are intended for the sole use of the named
> recipient(s) and contain(s) confidential information that may be
> proprietary, privileged or copyrighted under applicable law. If you are not
> the intended recipient, do not read, copy, or forward this email message or
> any attachments. Delete this email message and any attachments immediately.
>
>
>
> _______________________________________________
> ldv-project mailing list
> ldv-project at linuxtesting.org
> http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20190702/672256d6/attachment.html>
More information about the ldv-project
mailing list