Error Trace

[Home]

Bug # 156

Show/hide error trace
Error trace
Function bodies
Blocks
  • Others...
    Function bodies without model function calls
    Initialization function calls
    Initialization function bodies
    Entry point
    Entry point body
    Function calls
    Skipped function calls
    Formal parameter names
    Declarations
    Assumes
    Assume conditions
    Returns
    Return values
    DEG initialization
    DEG function calls
    Model function calls
    Model function bodies
    Model asserts
    Model state changes
    Model function function calls
    Model function function bodies
    Model returns
    Model others
    Identation
    Line numbers
    Expand signs
-entry_point
{
2301 ldv_s_mv_u3d_driver_platform_driver = 0;
2287 LDV_IN_INTERRUPT = 1;
2296 ldv_initialize() { /* Function call is skipped due to function is undefined */}
2306 goto ldv_34620;
2306 tmp___0 = nondet_int() { /* Function call is skipped due to function is undefined */}
2306 assume(tmp___0 != 0);
2309 goto ldv_34619;
2307 ldv_34619:;
2310 tmp = nondet_int() { /* Function call is skipped due to function is undefined */}
2310 switch (tmp);
2311 assume(!(tmp == 0));
2335 assume(!(tmp == 1));
2358 assume(!(tmp == 2));
2381 assume(!(tmp == 3));
2404 assume(!(tmp == 4));
2427 assume(!(tmp == 5));
2450 assume(!(tmp == 6));
2473 assume(!(tmp == 7));
2496 assume(!(tmp == 8));
2519 assume(!(tmp == 9));
2542 assume(!(tmp == 10));
2565 assume(!(tmp == 11));
2588 assume(!(tmp == 12));
2611 assume(!(tmp == 13));
2634 assume(!(tmp == 14));
2660 assume(!(tmp == 15));
2683 assume(!(tmp == 16));
2704 assume(tmp == 17);
2707 LDV_IN_INTERRUPT = 2;
2714 ldv_handler_precall() { /* Function call is skipped due to function is undefined */}
2715 -mv_u3d_irq(var_mv_u3d_irq_39_p0, var_mv_u3d_irq_39_p1)
{
1673 u3d = (struct mv_u3d *)dev;
1678 +spin_lock(&(u3d->lock))
1680 status = ioread32((void *)(&(u3d->vuc_regs->intrcause))) { /* Function call is skipped due to function is undefined */}
1681 intr = ioread32((void *)(&(u3d->vuc_regs->intrenable))) { /* Function call is skipped due to function is undefined */}
1682 status = status & intr;
1684 assume(!(status == 0U));
1690 assume((status & 65536U) != 0U);
1691 bridgesetting = ioread32((void *)(&(u3d->vuc_regs->bridgesetting))) { /* Function call is skipped due to function is undefined */}
1692 assume((bridgesetting & 65536U) != 0U);
1694 bridgesetting = 65536U;
1695 iowrite32(bridgesetting, (void *)(&(u3d->vuc_regs->bridgesetting))) { /* Function call is skipped due to function is undefined */}
1696 descriptor.modname = "mv_u3d_core";
1696 descriptor.function = "mv_u3d_irq";
1696 descriptor.filename = "/home/ldvuser/ldv/ref_launches/work/current--X--drivers--X--defaultlinux-4.8-rc1.tar.xz--X--331_1a--X--cpachecker/linux-4.8-rc1.tar.xz/csd_deg_dscv/10667/dscv_tempdir/dscv/ri/331_1a/drivers/usb/gadget/udc/mv_u3d_core.c";
1696 descriptor.format = "vbus valid\n";
1696 descriptor.lineno = 1696U;
1696 descriptor.flags = 0U;
1696 tmp = __builtin_expect(((long)(descriptor.flags)) & 1L, 0L) { /* Function call is skipped due to function is undefined */}
1696 assume(!(tmp != 0L));
1698 u3d->usb_state = 2U;
1699 u3d->vbus_valid_detect = 0U;
1703 unsigned long __CPAchecker_TMP_2 = (unsigned long)(u3d->vbus);
1703 assume(!(__CPAchecker_TMP_2 == ((unsigned long)((struct mv_usb_addon_irq *)0))));
1713 assume(!((status & 8U) != 0U));
1720 assume(!((status & 48U) != 0U));
1729 assume(!((status & 16777216U) != 0U));
1732 assume((status & 4U) != 0U);
1733 -mv_u3d_irq_process_tr_complete(u3d)
{
1610 ep_num = 0;
1610 direction = 0;
1615 tmp = ioread32((void *)(&(u3d->vuc_regs->endcomplete))) { /* Function call is skipped due to function is undefined */}
1617 descriptor.modname = "mv_u3d_core";
1617 descriptor.function = "mv_u3d_irq_process_tr_complete";
1617 descriptor.filename = "/home/ldvuser/ldv/ref_launches/work/current--X--drivers--X--defaultlinux-4.8-rc1.tar.xz--X--331_1a--X--cpachecker/linux-4.8-rc1.tar.xz/csd_deg_dscv/10667/dscv_tempdir/dscv/ri/331_1a/drivers/usb/gadget/udc/mv_u3d_core.c";
1617 descriptor.format = "tr_complete: ep: 0x%x\n";
1617 descriptor.lineno = 1617U;
1617 descriptor.flags = 0U;
1617 tmp___0 = __builtin_expect(((long)(descriptor.flags)) & 1L, 0L) { /* Function call is skipped due to function is undefined */}
1617 assume(!(tmp___0 != 0L));
1618 assume(!(tmp == 0U));
1620 iowrite32(tmp, (void *)(&(u3d->vuc_regs->endcomplete))) { /* Function call is skipped due to function is undefined */}
1622 i = 0;
1622 goto ldv_34487;
1622 assume(((unsigned int)i) < ((u3d->max_eps) * 2U));
1624 goto ldv_34486;
1623 ldv_34486:;
1623 ep_num = i >> 1;
1624 direction = i % 2;
1626 bit_pos = (u32 )(1 << ((direction * 16) + ep_num));
1628 assume(!((bit_pos & tmp) == 0U));
1631 assume(i == 0);
1632 curr_ep = (u3d->eps) + 1UL;
1637 descriptor___0.modname = "mv_u3d_core";
1637 descriptor___0.function = "mv_u3d_irq_process_tr_complete";
1637 descriptor___0.filename = "/home/ldvuser/ldv/ref_launches/work/current--X--drivers--X--defaultlinux-4.8-rc1.tar.xz--X--331_1a--X--cpachecker/linux-4.8-rc1.tar.xz/csd_deg_dscv/10667/dscv_tempdir/dscv/ri/331_1a/drivers/usb/gadget/udc/mv_u3d_core.c";
1637 descriptor___0.format = "tr comp: check req_list\n";
1637 descriptor___0.lineno = 1637U;
1637 descriptor___0.flags = 0U;
1637 tmp___1 = __builtin_expect(((long)(descriptor___0.flags)) & 1L, 0L) { /* Function call is skipped due to function is undefined */}
1637 assume(!(tmp___1 != 0L));
1638 +spin_lock(&(curr_ep->req_lock))
1639 +list_empty((const struct list_head *)(&(curr_ep->req_list)))
1639 assume(!(tmp___2 == 0));
1646 +spin_unlock(&(curr_ep->req_lock))
1649 __mptr___0 = (const struct list_head *)(curr_ep->queue.next);
1649 curr_req = ((struct mv_u3d_req *)__mptr___0) + 18446744073709551520UL;
1649 __mptr___1 = (const struct list_head *)(curr_req->queue.next);
1649 temp_req = ((struct mv_u3d_req *)__mptr___1) + 18446744073709551520UL;
1649 goto ldv_34484;
1649 assume(!(((unsigned long)(&(curr_req->queue))) != ((unsigned long)(&(curr_ep->queue)))));
1655 ldv_34482:;
1666 descriptor___1.modname = "mv_u3d_core";
1666 descriptor___1.function = "mv_u3d_irq_process_tr_complete";
1666 descriptor___1.filename = "/home/ldvuser/ldv/ref_launches/work/current--X--drivers--X--defaultlinux-4.8-rc1.tar.xz--X--331_1a--X--cpachecker/linux-4.8-rc1.tar.xz/csd_deg_dscv/10667/dscv_tempdir/dscv/ri/331_1a/drivers/usb/gadget/udc/mv_u3d_core.c";
1666 descriptor___1.format = "call mv_u3d_start_queue from ep complete\n";
1666 descriptor___1.lineno = 1666U;
1666 descriptor___1.flags = 0U;
1666 tmp___3 = __builtin_expect(((long)(descriptor___1.flags)) & 1L, 0L) { /* Function call is skipped due to function is undefined */}
1666 assume(!(tmp___3 != 0L));
1667 -mv_u3d_start_queue(curr_ep)
{
476 u3d = ep->u3d;
480 +list_empty((const struct list_head *)(&(ep->req_list)))
480 assume(tmp == 0);
480 assume((ep->processing) == 0U);
481 __mptr = (const struct list_head *)(ep->req_list.next);
481 req = ((struct mv_u3d_req *)__mptr) + 18446744073709551504UL;
485 ep->processing = 1U;
488 assume(((unsigned int)(*(((unsigned short *)ep) + 108UL))) == 0U);
488 int __CPAchecker_TMP_1 = (int)(ep->u3d->ep0_dir);
488 __CPAchecker_TMP_0 = __CPAchecker_TMP_1;
488 ret = usb_gadget_map_request(&(u3d->gadget), &(req->req), __CPAchecker_TMP_0) { /* Function call is skipped due to function is undefined */}
490 assume(!(ret != 0));
493 req->req.status = -115;
494 req->req.actual = 0U;
495 req->trb_count = 0U;
498 -mv_u3d_req_to_trb(req)
{
415 u3d = req->ep->u3d;
417 +INIT_LIST_HEAD(&(req->trb_list))
419 length = (req->req.length) - (req->req.actual);
423 assume(!(length <= 65536U));
430 trb_num = length / 65536U;
431 assume(!((length & 65535U) != 0U));
434 +kcalloc((size_t )trb_num, 32UL, 34078752U)
434 trb = (struct mv_u3d_trb *)tmp;
435 assume(!(((unsigned long)trb) == ((unsigned long)((struct mv_u3d_trb *)0))));
438 +kcalloc((size_t )trb_num, 16UL, 34078752U)
438 trb_hw = (struct mv_u3d_trb_hw *)tmp___0;
439 assume(!(((unsigned long)trb_hw) == ((unsigned long)((struct mv_u3d_trb_hw *)0))));
445 ldv_34100:;
445 trb->trb_hw = trb_hw;
446 +mv_u3d_build_trb_chain(req, &count, trb, &is_last)
446 assume(!(tmp___1 != 0));
454 +list_add_tail(&(trb->trb_list), &(req->trb_list))
455 req->trb_count = (req->trb_count) + 1U;
456 trb = trb + 1;
457 trb_hw = trb_hw + 1;
458 assume(!(is_last == 0));
460 __mptr = (const struct list_head *)(req->trb_list.next);
460 req->trb_head = ((struct mv_u3d_trb *)__mptr) + 18446744073709551600UL;
462 void *__CPAchecker_TMP_1 = (void *)(req->trb_head->trb_hw);
462 -dma_map_single_attrs(u3d->gadget.dev.parent, __CPAchecker_TMP_1, ((unsigned long)trb_num) * 16UL, 0, 0UL)
{
38 -ldv_dma_map_page()
{
10 assume(!(LDV_DMA_MAP_CALLS != 0));
12 LDV_DMA_MAP_CALLS = LDV_DMA_MAP_CALLS + 1;
13 return ;;
}
40 +ldv_dma_map_single_attrs_5(dev, ptr, size, dir, attrs)
40 return tmp;;
}
467 req->chain = 1U;
470 return 0;;
}
498 assume(tmp___0 == 0);
499 +mv_u3d_queue_trb(ep, req)
500 assume(!(ret != 0));
511 assume(((unsigned long)req) != ((unsigned long)((struct mv_u3d_req *)0)));
512 +list_add_tail(&(req->queue), &(ep->queue))
514 return 0;;
}
1668 ldv_34471:;
1622 i = i + 1;
1623 ldv_34487:;
1622 assume(((unsigned int)i) < ((u3d->max_eps) * 2U));
1624 goto ldv_34486;
1623 ldv_34486:;
1623 ep_num = i >> 1;
1624 direction = i % 2;
1626 bit_pos = (u32 )(1 << ((direction * 16) + ep_num));
1628 assume(!((bit_pos & tmp) == 0U));
1631 assume(!(i == 0));
1634 curr_ep = (u3d->eps) + ((unsigned long)i);
1637 descriptor___0.modname = "mv_u3d_core";
1637 descriptor___0.function = "mv_u3d_irq_process_tr_complete";
1637 descriptor___0.filename = "/home/ldvuser/ldv/ref_launches/work/current--X--drivers--X--defaultlinux-4.8-rc1.tar.xz--X--331_1a--X--cpachecker/linux-4.8-rc1.tar.xz/csd_deg_dscv/10667/dscv_tempdir/dscv/ri/331_1a/drivers/usb/gadget/udc/mv_u3d_core.c";
1637 descriptor___0.format = "tr comp: check req_list\n";
1637 descriptor___0.lineno = 1637U;
1637 descriptor___0.flags = 0U;
1637 tmp___1 = __builtin_expect(((long)(descriptor___0.flags)) & 1L, 0L) { /* Function call is skipped due to function is undefined */}
1637 assume(!(tmp___1 != 0L));
1638 +spin_lock(&(curr_ep->req_lock))
1639 +list_empty((const struct list_head *)(&(curr_ep->req_list)))
1639 assume(!(tmp___2 == 0));
1646 +spin_unlock(&(curr_ep->req_lock))
1649 __mptr___0 = (const struct list_head *)(curr_ep->queue.next);
1649 curr_req = ((struct mv_u3d_req *)__mptr___0) + 18446744073709551520UL;
1649 __mptr___1 = (const struct list_head *)(curr_req->queue.next);
1649 temp_req = ((struct mv_u3d_req *)__mptr___1) + 18446744073709551520UL;
1649 goto ldv_34484;
1649 assume(!(((unsigned long)(&(curr_req->queue))) != ((unsigned long)(&(curr_ep->queue)))));
1655 ldv_34482:;
1666 descriptor___1.modname = "mv_u3d_core";
1666 descriptor___1.function = "mv_u3d_irq_process_tr_complete";
1666 descriptor___1.filename = "/home/ldvuser/ldv/ref_launches/work/current--X--drivers--X--defaultlinux-4.8-rc1.tar.xz--X--331_1a--X--cpachecker/linux-4.8-rc1.tar.xz/csd_deg_dscv/10667/dscv_tempdir/dscv/ri/331_1a/drivers/usb/gadget/udc/mv_u3d_core.c";
1666 descriptor___1.format = "call mv_u3d_start_queue from ep complete\n";
1666 descriptor___1.lineno = 1666U;
1666 descriptor___1.flags = 0U;
1666 tmp___3 = __builtin_expect(((long)(descriptor___1.flags)) & 1L, 0L) { /* Function call is skipped due to function is undefined */}
1666 assume(!(tmp___3 != 0L));
1667 -mv_u3d_start_queue(curr_ep)
{
476 u3d = ep->u3d;
480 +list_empty((const struct list_head *)(&(ep->req_list)))
480 assume(tmp == 0);
480 assume((ep->processing) == 0U);
481 __mptr = (const struct list_head *)(ep->req_list.next);
481 req = ((struct mv_u3d_req *)__mptr) + 18446744073709551504UL;
485 ep->processing = 1U;
488 assume(((unsigned int)(*(((unsigned short *)ep) + 108UL))) == 0U);
488 int __CPAchecker_TMP_1 = (int)(ep->u3d->ep0_dir);
488 __CPAchecker_TMP_0 = __CPAchecker_TMP_1;
488 ret = usb_gadget_map_request(&(u3d->gadget), &(req->req), __CPAchecker_TMP_0) { /* Function call is skipped due to function is undefined */}
490 assume(!(ret != 0));
493 req->req.status = -115;
494 req->req.actual = 0U;
495 req->trb_count = 0U;
498 -mv_u3d_req_to_trb(req)
{
415 u3d = req->ep->u3d;
417 +INIT_LIST_HEAD(&(req->trb_list))
419 length = (req->req.length) - (req->req.actual);
423 assume(!(length <= 65536U));
430 trb_num = length / 65536U;
431 assume((length & 65535U) != 0U);
432 trb_num = trb_num + 1U;
434 +kcalloc((size_t )trb_num, 32UL, 34078752U)
434 trb = (struct mv_u3d_trb *)tmp;
435 assume(!(((unsigned long)trb) == ((unsigned long)((struct mv_u3d_trb *)0))));
438 +kcalloc((size_t )trb_num, 16UL, 34078752U)
438 trb_hw = (struct mv_u3d_trb_hw *)tmp___0;
439 assume(!(((unsigned long)trb_hw) == ((unsigned long)((struct mv_u3d_trb_hw *)0))));
445 ldv_34100:;
445 trb->trb_hw = trb_hw;
446 +mv_u3d_build_trb_chain(req, &count, trb, &is_last)
446 assume(!(tmp___1 != 0));
454 +list_add_tail(&(trb->trb_list), &(req->trb_list))
455 req->trb_count = (req->trb_count) + 1U;
456 trb = trb + 1;
457 trb_hw = trb_hw + 1;
458 assume(!(is_last == 0));
460 __mptr = (const struct list_head *)(req->trb_list.next);
460 req->trb_head = ((struct mv_u3d_trb *)__mptr) + 18446744073709551600UL;
462 void *__CPAchecker_TMP_1 = (void *)(req->trb_head->trb_hw);
462 -dma_map_single_attrs(u3d->gadget.dev.parent, __CPAchecker_TMP_1, ((unsigned long)trb_num) * 16UL, 0, 0UL)
{
38 -ldv_dma_map_page()
{
10 assume(LDV_DMA_MAP_CALLS != 0);
10 +ldv_error()
}
}
}
}
}
}
}
Source code
1 #ifndef _ASM_X86_DMA_MAPPING_H 2 #define _ASM_X86_DMA_MAPPING_H 3 4 /* 5 * IOMMU interface. See Documentation/DMA-API-HOWTO.txt and 6 * Documentation/DMA-API.txt for documentation. 7 */ 8 9 #include <linux/kmemcheck.h> 10 #include <linux/scatterlist.h> 11 #include <linux/dma-debug.h> 12 #include <asm/io.h> 13 #include <asm/swiotlb.h> 14 #include <linux/dma-contiguous.h> 15 16 #ifdef CONFIG_ISA 17 # define ISA_DMA_BIT_MASK DMA_BIT_MASK(24) 18 #else 19 # define ISA_DMA_BIT_MASK DMA_BIT_MASK(32) 20 #endif 21 22 #define DMA_ERROR_CODE 0 23 24 extern int iommu_merge; 25 extern struct device x86_dma_fallback_dev; 26 extern int panic_on_overflow; 27 28 extern struct dma_map_ops *dma_ops; 29 30 static inline struct dma_map_ops *get_dma_ops(struct device *dev) 31 { 32 #ifndef CONFIG_X86_DEV_DMA_OPS 33 return dma_ops; 34 #else 35 if (unlikely(!dev) || !dev->archdata.dma_ops) 36 return dma_ops; 37 else 38 return dev->archdata.dma_ops; 39 #endif 40 } 41 42 bool arch_dma_alloc_attrs(struct device **dev, gfp_t *gfp); 43 #define arch_dma_alloc_attrs arch_dma_alloc_attrs 44 45 #define HAVE_ARCH_DMA_SUPPORTED 1 46 extern int dma_supported(struct device *hwdev, u64 mask); 47 48 extern void *dma_generic_alloc_coherent(struct device *dev, size_t size, 49 dma_addr_t *dma_addr, gfp_t flag, 50 unsigned long attrs); 51 52 extern void dma_generic_free_coherent(struct device *dev, size_t size, 53 void *vaddr, dma_addr_t dma_addr, 54 unsigned long attrs); 55 56 #ifdef CONFIG_X86_DMA_REMAP /* Platform code defines bridge-specific code */ 57 extern bool dma_capable(struct device *dev, dma_addr_t addr, size_t size); 58 extern dma_addr_t phys_to_dma(struct device *dev, phys_addr_t paddr); 59 extern phys_addr_t dma_to_phys(struct device *dev, dma_addr_t daddr); 60 #else 61 62 static inline bool dma_capable(struct device *dev, dma_addr_t addr, size_t size) 63 { 64 if (!dev->dma_mask) 65 return 0; 66 67 return addr + size - 1 <= *dev->dma_mask; 68 } 69 70 static inline dma_addr_t phys_to_dma(struct device *dev, phys_addr_t paddr) 71 { 72 return paddr; 73 } 74 75 static inline phys_addr_t dma_to_phys(struct device *dev, dma_addr_t daddr) 76 { 77 return daddr; 78 } 79 #endif /* CONFIG_X86_DMA_REMAP */ 80 81 static inline void 82 dma_cache_sync(struct device *dev, void *vaddr, size_t size, 83 enum dma_data_direction dir) 84 { 85 flush_write_buffers(); 86 } 87 88 static inline unsigned long dma_alloc_coherent_mask(struct device *dev, 89 gfp_t gfp) 90 { 91 unsigned long dma_mask = 0; 92 93 dma_mask = dev->coherent_dma_mask; 94 if (!dma_mask) 95 dma_mask = (gfp & GFP_DMA) ? DMA_BIT_MASK(24) : DMA_BIT_MASK(32); 96 97 return dma_mask; 98 } 99 100 static inline gfp_t dma_alloc_coherent_gfp_flags(struct device *dev, gfp_t gfp) 101 { 102 unsigned long dma_mask = dma_alloc_coherent_mask(dev, gfp); 103 104 if (dma_mask <= DMA_BIT_MASK(24)) 105 gfp |= GFP_DMA; 106 #ifdef CONFIG_X86_64 107 if (dma_mask <= DMA_BIT_MASK(32) && !(gfp & GFP_DMA)) 108 gfp |= GFP_DMA32; 109 #endif 110 return gfp; 111 } 112 113 #endif

Here is an explanation of a rule violation arisen while checking your driver against a corresponding kernel.

Note that it may be false positive, i.e. there isn't a real error indeed. Please analyze a given error trace and related source code to understand whether there is an error in your driver.

Error trace column contains a path on which the given rule is violated. You can expand/collapse some entity classes by clicking on corresponding checkboxes in a main menu or in an advanced Others menu. Also you can expand/collapse each particular entity by clicking on +/-. In hovering on some entities you can see some tips. Also the error trace is bound with related source code. Line numbers may be shown as links on the left. You can click on them to open corresponding lines in source code.

Source code column contains a content of files related with the error trace. There is source code of your driver (note that there are some LDV modifications at the end), kernel headers and rule model. Tabs show a currently opened file and other available files. In hovering on them you can see full file names. On clicking a corresponding file content will be shown.

Kernel Module Rule Verifier Verdict Status Timestamp Bug report
linux-4.8-rc1.tar.xz drivers/usb/gadget/udc/mv_u3d_core.ko 331_1a CPAchecker Bug Fixed 2016-10-29 02:14:15 L0254

Comment

Reported: 29 Oct 2016

[Home]